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 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 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 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 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 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 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 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 S1[ 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 S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
proof
let B be Element of Fin C; :: thesis: for b being Element of C st S1[B] & not b in B holds
S1[B \/ {.b.}]

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