consider x being Element of X;
deffunc H₁( Element of X, Element of X) -> Element of X = IFEQ X,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,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:19, FINSEQ_2:154, RELSET_1:11;
arity f = 2 by A3, COMPUT_1:27;
then reconsider f = f as non empty homogeneous quasi_total PartFunc of (X * ),X by A3, COMPUT_1:25;
take f ; :: thesis: ( f is binary & f is associative & f is unital )
thus arity f = 2 by A3, COMPUT_1:27; :: according to COMPUT_1:def 26 :: 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:158;
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 = x implies IFEQ u,x,y,u = y ) by FUNCOP_1:def 8;
A7: ( u <> x implies IFEQ u,x,y,u = u ) by FUNCOP_1:def 8;
A8: ( u = x implies IFEQ u,x,(IFEQ y,x,z,y),u = IFEQ y,x,z,y ) by FUNCOP_1:def 8;
A9: ( u <> x implies IFEQ u,x,(IFEQ y,x,z,y),u = u ) by FUNCOP_1:def 8;
A10: ( u <> x implies IFEQ u,x,z,u = u ) by FUNCOP_1:def 8;
thus f . <*(f . <*u,y*>),z*> = f . <*(IFEQ u9,x,y9,u9),z9*> by A1
.= IFEQ (IFEQ u,x,y,u),x,z,(IFEQ u,x,y,u) by A1
.= f . <*u9,(IFEQ y9,x,z9,y9)*> by A1, A6, A7, A8, A9, A10
.= f . <*u,(f . <*y,z*>)*> by A1 ; :: thesis: verum

end;

take x ; :: according to AOFA_000:def 3 :: thesis: 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 ( <*x,y*> in dom f & f . <*x,y*> = y & <*y,x*> in dom f & f . <*y,x*> = y ) )
assume ( <*y,z*> in dom f or <*z,y*> in dom f ) ; :: thesis: ( <*x,y*> in dom f & f . <*x,y*> = y & <*y,x*> in dom f & f . <*y,x*> = y )
then reconsider y9 = y as Element of X by A3, FINSEQ_2:158;
<*x,y9*> in 2 -tuples_on X by FINSEQ_2:157;
hence <*x,y*> in dom f by FUNCT_2:def 1; :: thesis: ( f . <*x,y*> = y & <*y,x*> in dom f & f . <*y,x*> = y )
thus f . <*x,y*> = IFEQ x,x,y9,x by A1
.= y by FUNCOP_1:def 8 ; :: thesis: ( <*y,x*> in dom f & f . <*y,x*> = y )
<*y9,x*> in 2 -tuples_on X by FINSEQ_2:157;
hence <*y,x*> in dom f by FUNCT_2:def 1; :: thesis: f . <*y,x*> = y
A11: ( x = y or x <> y ) ;
thus f . <*y,x*> = IFEQ y9,x,x,y9 by A1
.= y by A11, FUNCOP_1:def 8 ; :: thesis: verum