let C, D be non empty set ; :: thesis:
let B be Element of Fin C; :: thesis:
let e be Element of D; :: thesis:
let F, G be BinOp of D; :: thesis:
let f, f9 be Function of C,D; :: thesis:
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: e = the_unity_wrt F and
A3: G . (e,e) = e and
A4: for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ; :: thesis:
defpred S₁[ Element of Fin C] means G . ((F $$ ($1,f)),(F $$ ($1,f9))) = F $$ ($1,(G .: (f,f9)));
A5: for B9 being Element of Fin C
for b being Element of C st S₁[B9] & not b in B9 holds
S₁[B9 \/ {.b.}]

let B be Element of Fin C; :: thesis:
let c be Element of C; :: thesis:
assume that
A6: G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) and
A7: not c in B ; :: thesis:
set s9 = F $$ (B,f9);
set s = F $$ (B,f);
( F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c)) & F $$ ((B \/ {.c.}),f9) = F . ((F $$ (B,f9)),(f9 . c)) ) by A1, A7, Th2;
hence G . ((F $$ ((B \/ {.c.}),f)),(F $$ ((B \/ {.c.}),f9))) = F . ((G . ((F $$ (B,f)),(F $$ (B,f9)))),(G . ((f . c),(f9 . c)))) by A4
.= F . ((G . ((F $$ (B,f)),(F $$ (B,f9)))),((G .: (f,f9)) . c)) by FUNCOP_1:37
.= F $$ ((B \/ {.c.}),(G .: (f,f9))) by A1, A6, A7, Th2 ;
:: thesis:

end;

( F $$ (({}. C),f) = e & F $$ (({}. C),f9) = e ) by A1, A2, SETWISEO:31;
then A8: S₁[ {}. C] by A1, A2, A3, SETWISEO:31;
for B being Element of Fin C holds S₁[B] from SETWISEO:sch 2(A8, A5);
hence G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) ; :: thesis: