set x = the Element of X;
deffunc H₁( Element of X, Element of X) -> Element of X = IFEQ (X, the Element of X,c₂,X);
( ex f being Function of (2 -tuples_on X),X st
for x, y being Element of X holds f . <*x,y*> = H₁(x,y) & ( for f1, f2 being Function of (2 -tuples_on X),X st ( for x, y being Element of X holds f1 . <*x,y*> = H₁(x,y) ) & ( for x, y being Element of X holds f2 . <*x,y*> = H₁(x,y) ) holds
f1 = f2 ) ) from CIRCCMB3:sch 7();
then consider f being Function of (2 -tuples_on X),X such that
A1: for a, b being Element of X holds f . <*a,b*> = IFEQ (a, the Element of X,b,a) ;
A2: rng f c= X ;
A3: dom f = 2 -tuples_on X by FUNCT_2:def 1;
then reconsider f = f as non empty homogeneous PartFunc of (X *),X by A2, COMPUT_1:16, FINSEQ_2:134, RELSET_1:4;
arity f = 2 by A3, COMPUT_1:24;
then reconsider f = f as non empty homogeneous quasi_total PartFunc of (X *),X by A3, COMPUT_1:22;
take f ; :: thesis: ( f is 2 -ary & f is associative & f is unital )
thus arity f = 2 by A3, COMPUT_1:24; :: according to COMPUT_1:def 21 :: thesis: ( f is associative & f is unital )

hereby :: according to AOFA_000:def 2 :: thesis: f is unital

let u, y, z be set ; :: thesis: ( <*u,y*> in dom f & <*y,z*> in dom f & <*(f . <*u,y*>),z*> in dom f & <*u,(f . <*y,z*>)*> in dom f implies f . <*(f . <*u,y*>),z*> = f . <*u,(f . <*y,z*>)*> )
assume that
A4: <*u,y*> in dom f and
A5: <*y,z*> in dom f ; :: thesis: ( <*(f . <*u,y*>),z*> in dom f & <*u,(f . <*y,z*>)*> in dom f implies f . <*(f . <*u,y*>),z*> = f . <*u,(f . <*y,z*>)*> )
reconsider u9 = u, y9 = y, z9 = z as Element of X by A3, A4, A5, FINSEQ_2:138;
assume that
<*(f . <*u,y*>),z*> in dom f and
<*u,(f . <*y,z*>)*> in dom f ; :: thesis: f . <*(f . <*u,y*>),z*> = f . <*u,(f . <*y,z*>)*>
A6: ( u = the Element of X implies IFEQ (u, the Element of X,y,u) = y ) by FUNCOP_1:def 8;
A7: ( u <> the Element of X implies IFEQ (u, the Element of X,y,u) = u ) by FUNCOP_1:def 8;
A8: ( u = the Element of X implies IFEQ (u, the Element of X,(IFEQ (y, the Element of X,z,y)),u) = IFEQ (y, the Element of X,z,y) ) by FUNCOP_1:def 8;
A9: ( u <> the Element of X implies IFEQ (u, the Element of X,(IFEQ (y, the Element of X,z,y)),u) = u ) by FUNCOP_1:def 8;
A10: ( u <> the Element of X implies IFEQ (u, the Element of X,z,u) = u ) by FUNCOP_1:def 8;
thus f . <*(f . <*u,y*>),z*> = f . <*(IFEQ (u9, the Element of X,y9,u9)),z9*> by A1
.= IFEQ ((IFEQ (u, the Element of X,y,u)), the Element of X,z,(IFEQ (u, the Element of X,y,u))) by A1
.= f . <*u9,(IFEQ (y9, the Element of X,z9,y9))*> by A1, A6, A7, A8, A9, A10
.= f . <*u,(f . <*y,z*>)*> by A1 ; :: thesis: verum

end;

take the Element of X ; :: according to AOFA_000:def 3 :: thesis: the Element of X is_a_unity_wrt f
let y, z be set ; :: according to AOFA_000:def 1 :: thesis: ( ( <*y,z*> in dom f or <*z,y*> in dom f ) implies ( <* the Element of X,y*> in dom f & f . <* the Element of X,y*> = y & <*y, the Element of X*> in dom f & f . <*y, the Element of X*> = y ) )
assume ( <*y,z*> in dom f or <*z,y*> in dom f ) ; :: thesis: ( <* the Element of X,y*> in dom f & f . <* the Element of X,y*> = y & <*y, the Element of X*> in dom f & f . <*y, the Element of X*> = y )
then reconsider y9 = y as Element of X by A3, FINSEQ_2:138;
<* the Element of X,y9*> in 2 -tuples_on X by FINSEQ_2:137;
hence <* the Element of X,y*> in dom f by FUNCT_2:def 1; :: thesis: ( f . <* the Element of X,y*> = y & <*y, the Element of X*> in dom f & f . <*y, the Element of X*> = y )
thus f . <* the Element of X,y*> = IFEQ ( the Element of X, the Element of X,y9, the Element of X) by A1
.= y by FUNCOP_1:def 8 ; :: thesis: ( <*y, the Element of X*> in dom f & f . <*y, the Element of X*> = y )
<*y9, the Element of X*> in 2 -tuples_on X by FINSEQ_2:137;
hence <*y, the Element of X*> in dom f by FUNCT_2:def 1; :: thesis: f . <*y, the Element of X*> = y
A11: ( the Element of X = y or the Element of X <> y ) ;
thus f . <*y, the Element of X*> = IFEQ (y9, the Element of X, the Element of X,y9) by A1
.= y by A11, FUNCOP_1:def 8 ; :: thesis: verum