let C, D be non empty set ; :: thesis: for B being Element of Fin C

for e being Element of D

for F, G being BinOp of D

for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds

G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))

let B be Element of Fin C; :: thesis: for e being Element of D

for F, G being BinOp of D

for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds

G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))

let e be Element of D; :: thesis: for F, G being BinOp of D

for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds

G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))

let F, G be BinOp of D; :: thesis: for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds

G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))

let f, f9 be Function of C,D; :: thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) implies G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) )

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: G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))

defpred S_{1}[ 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_{1}[B9] & not b in B9 holds

S_{1}[B9 \/ {.b.}]

then A8: S_{1}[ {}. C]
by A1, A2, A3, SETWISEO:31;

for B being Element of Fin C holds S_{1}[B]
from SETWISEO:sch 2(A8, A5);

hence G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) ; :: thesis: verum

for e being Element of D

for F, G being BinOp of D

for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds

G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))

let B be Element of Fin C; :: thesis: for e being Element of D

for F, G being BinOp of D

for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds

G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))

let e be Element of D; :: thesis: for F, G being BinOp of D

for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds

G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))

let F, G be BinOp of D; :: thesis: for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) holds

G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))

let f, f9 be Function of C,D; :: thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . (e,e) = e & ( for d1, d2, d3, d4 being Element of D holds F . ((G . (d1,d2)),(G . (d3,d4))) = G . ((F . (d1,d3)),(F . (d2,d4))) ) implies G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) )

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: G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))

defpred S

A5: for B9 being Element of Fin C

for b being Element of C st S

S

proof

( F $$ (({}. C),f) = e & F $$ (({}. C),f9) = e )
by A1, A2, SETWISEO:31;
let B be Element of Fin C; :: thesis: for b being Element of C st S_{1}[B] & not b in B holds

S_{1}[B \/ {.b.}]

let c be Element of C; :: thesis: ( S_{1}[B] & not c in B implies S_{1}[B \/ {.c.}] )

assume that

A6: G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) and

A7: not c in B ; :: thesis: S_{1}[B \/ {.c.}]

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: verum

end;S

let c be Element of C; :: thesis: ( S

assume that

A6: G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) and

A7: not c in B ; :: thesis: S

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: verum

then A8: S

for B being Element of Fin C holds S

hence G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9))) ; :: thesis: verum