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

for F being BinOp of D

for f being Function of C,D

for H being BinOp of E

for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F $$ (B,f)) = H $$ (B,(h * f))

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

for f being Function of C,D

for H being BinOp of E

for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F $$ (B,f)) = H $$ (B,(h * f))

let F be BinOp of D; :: thesis: for f being Function of C,D

for H being BinOp of E

for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F $$ (B,f)) = H $$ (B,(h * f))

let f be Function of C,D; :: thesis: for H being BinOp of E

for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F $$ (B,f)) = H $$ (B,(h * f))

let H be BinOp of E; :: thesis: for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F $$ (B,f)) = H $$ (B,(h * f))

let h be Function of D,E; :: thesis: ( F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h . (F $$ (B,f)) = H $$ (B,(h * f)) )

assume that

A1: ( F is commutative & F is associative & F is having_a_unity ) and

A2: ( H is commutative & H is associative & H is having_a_unity ) and

A3: h . (the_unity_wrt F) = the_unity_wrt H and

A4: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; :: thesis: h . (F $$ (B,f)) = H $$ (B,(h * f))

defpred S_{1}[ Element of Fin C] means h . (F $$ ($1,f)) = H $$ ($1,(h * f));

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.}]

.= H $$ (({}. C),(h * f)) by A2, SETWISEO:31 ;

then A8: S_{1}[ {}. C]
;

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

hence h . (F $$ (B,f)) = H $$ (B,(h * f)) ; :: thesis: verum

for F being BinOp of D

for f being Function of C,D

for H being BinOp of E

for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F $$ (B,f)) = H $$ (B,(h * f))

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

for f being Function of C,D

for H being BinOp of E

for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F $$ (B,f)) = H $$ (B,(h * f))

let F be BinOp of D; :: thesis: for f being Function of C,D

for H being BinOp of E

for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F $$ (B,f)) = H $$ (B,(h * f))

let f be Function of C,D; :: thesis: for H being BinOp of E

for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F $$ (B,f)) = H $$ (B,(h * f))

let H be BinOp of E; :: thesis: for h being Function of D,E st F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F $$ (B,f)) = H $$ (B,(h * f))

let h be Function of D,E; :: thesis: ( F is commutative & F is associative & F is having_a_unity & H is commutative & H is associative & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h . (F $$ (B,f)) = H $$ (B,(h * f)) )

assume that

A1: ( F is commutative & F is associative & F is having_a_unity ) and

A2: ( H is commutative & H is associative & H is having_a_unity ) and

A3: h . (the_unity_wrt F) = the_unity_wrt H and

A4: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; :: thesis: h . (F $$ (B,f)) = H $$ (B,(h * f))

defpred S

A5: for B9 being Element of Fin C

for b being Element of C st S

S

proof

h . (F $$ (({}. C),f)) =
the_unity_wrt H
by A1, A3, 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: h . (F $$ (B,f)) = H $$ (B,(h * f)) and

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

thus h . (F $$ ((B \/ {.c.}),f)) = h . (F . ((F $$ (B,f)),(f . c))) by A1, A7, Th2

.= H . ((H $$ (B,(h * f))),(h . (f . c))) by A4, A6

.= H . ((H $$ (B,(h * f))),((h * f) . c)) by FUNCT_2:15

.= H $$ ((B \/ {.c.}),(h * f)) by A2, A7, Th2 ; :: thesis: verum

end;S

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

assume that

A6: h . (F $$ (B,f)) = H $$ (B,(h * f)) and

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

thus h . (F $$ ((B \/ {.c.}),f)) = h . (F . ((F $$ (B,f)),(f . c))) by A1, A7, Th2

.= H . ((H $$ (B,(h * f))),(h . (f . c))) by A4, A6

.= H . ((H $$ (B,(h * f))),((h * f) . c)) by FUNCT_2:15

.= H $$ ((B \/ {.c.}),(h * f)) by A2, A7, Th2 ; :: thesis: verum

.= H $$ (({}. C),(h * f)) by A2, SETWISEO:31 ;

then A8: S

for B being Element of Fin C holds S

hence h . (F $$ (B,f)) = H $$ (B,(h * f)) ; :: thesis: verum