6.8 Introduction of structure

Let (X,a) be a binominal algebra. In such a case (X is a set and a is a function), we write only the following (without useing definition etc.).

     struct Binalg(# base->set,op2->Function #);

For the new terminology Binalg, base, and op2, we write the following in a VOC file (be careful of adding the classification Symbol of G, U).

      GBinalg
      Ubase
      Uop2

    Then, the following theorem is formed without giving reason.

      theorem for X being set, a being Function
      holds (the base of Binalg(# X,a #))=X;

This corresponds to the proposition "the base of a binominal algebra (X, a) is X". Take care of adding the to base.