let C, E, D 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, Th4
.= H . (H $$ B,(h * f)),(h . (f . c)) by A4, A6
.= H . (H $$ B,(h * f)),((h * f) . c) by FUNCT_2:21
.= H $$ (B \/ {.c.}),(h * f) by A2, A7, Th4 ; :: thesis: verum

end;

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