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.