let C, D be non empty set ; :: thesis: for B being Element of Fin C
for d, e being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
let B be Element of Fin C; :: thesis: for d, e being Element of D
for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
let d, e be Element of D; :: thesis: for F, G being BinOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
let F, G be BinOp of D; :: thesis: for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e holds
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
let f be Function of C,D; :: thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G . (e,d) = e implies G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d))) )
assume that
A1: ( F is commutative & F is associative & F is having_a_unity ) and
A2: e = the_unity_wrt F and
A3: G is_distributive_wrt F ; :: thesis: ( not G . (e,d) = e or G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d))) )
defpred S₁[ Element of Fin C] means G . ((F $$ ($1,f)),d) = F $$ ($1,(G [:] (f,d)));
A4: 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 B9 be Element of Fin C; :: thesis: for b being Element of C st S₁[B9] & not b in B9 holds
S₁[B9 \/ {.b.}]
let c be Element of C; :: thesis: ( S₁[B9] & not c in B9 implies S₁[B9 \/ {.c.}] )
assume that
A5: G . ((F $$ (B9,f)),d) = F $$ (B9,(G [:] (f,d))) and
A6: not c in B9 ; :: thesis: S₁[B9 \/ {.c.}]
thus G . ((F $$ ((B9 \/ {.c.}),f)),d) = G . ((F . ((F $$ (B9,f)),(f . c))),d) by A1, A6, Th2
.= F . ((G . ((F $$ (B9,f)),d)),(G . ((f . c),d))) by A3, BINOP_1:11
.= F . ((F $$ (B9,(G [:] (f,d)))),((G [:] (f,d)) . c)) by A5, FUNCOP_1:48
.= F $$ ((B9 \/ {.c.}),(G [:] (f,d))) by A1, A6, Th2 ; :: thesis: verum

end;

assume G . (e,d) = e ; :: thesis: G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
then G . ((F $$ (({}. C),f)),d) = e by A1, A2, SETWISEO:31
.= F $$ (({}. C),(G [:] (f,d))) by A1, A2, SETWISEO:31 ;
then A7: S₁[ {}. C] ;
for B being Element of Fin C holds S₁[B] from SETWISEO:sch 2(A7, A4);
hence G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d))) ; :: thesis: verum