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₁[ 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₁[B9] & not b in B9 holds
S₁[B9 \/ {.b.}]

proof

let B be Element of Fin C; :: thesis: for b being Element of C st S₁[B] & not b in B holds
S₁[B \/ {.b.}]
let c be Element of C; :: thesis: ( S₁[B] & not c in B implies S₁[B \/ {.c.}] )
assume that
A6: h . (F $$ (B,f)) = H $$ (B,(h * f)) and
A7: not c in B ; :: thesis: S₁[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;

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