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 . (d,e) = e holds

G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,e) = e holds

G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,e) = e holds

G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,e) = e holds

G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,e) = e implies G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) )

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 . (d,e) = e or G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) )

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

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

then G . (d,(F $$ (({}. C),f))) = e by A1, A2, SETWISEO:31

.= F $$ (({}. C),(G [;] (d,f))) by A1, A2, SETWISEO:31 ;

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

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

hence G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) ; :: thesis: verum

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 . (d,e) = e holds

G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,e) = e holds

G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,e) = e holds

G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,e) = e holds

G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))

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 . (d,e) = e implies G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) )

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 . (d,e) = e or G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) )

defpred S

A4: for B9 being Element of Fin C

for b being Element of C st S

S

proof

assume
G . (d,e) = e
; :: thesis: G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f)))
let B9 be Element of Fin C; :: thesis: for b being Element of C st S_{1}[B9] & not b in B9 holds

S_{1}[B9 \/ {.b.}]

let c be Element of C; :: thesis: ( S_{1}[B9] & not c in B9 implies S_{1}[B9 \/ {.c.}] )

assume that

A5: G . (d,(F $$ (B9,f))) = F $$ (B9,(G [;] (d,f))) and

A6: not c in B9 ; :: thesis: S_{1}[B9 \/ {.c.}]

thus G . (d,(F $$ ((B9 \/ {.c.}),f))) = G . (d,(F . ((F $$ (B9,f)),(f . c)))) by A1, A6, Th2

.= F . ((G . (d,(F $$ (B9,f)))),(G . (d,(f . c)))) by A3, BINOP_1:11

.= F . ((F $$ (B9,(G [;] (d,f)))),((G [;] (d,f)) . c)) by A5, FUNCOP_1:53

.= F $$ ((B9 \/ {.c.}),(G [;] (d,f))) by A1, A6, Th2 ; :: thesis: verum

end;S

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

assume that

A5: G . (d,(F $$ (B9,f))) = F $$ (B9,(G [;] (d,f))) and

A6: not c in B9 ; :: thesis: S

thus G . (d,(F $$ ((B9 \/ {.c.}),f))) = G . (d,(F . ((F $$ (B9,f)),(f . c)))) by A1, A6, Th2

.= F . ((G . (d,(F $$ (B9,f)))),(G . (d,(f . c)))) by A3, BINOP_1:11

.= F . ((F $$ (B9,(G [;] (d,f)))),((G [;] (d,f)) . c)) by A5, FUNCOP_1:53

.= F $$ ((B9 \/ {.c.}),(G [;] (d,f))) by A1, A6, Th2 ; :: thesis: verum

then G . (d,(F $$ (({}. C),f))) = e by A1, A2, SETWISEO:31

.= F $$ (({}. C),(G [;] (d,f))) by A1, A2, SETWISEO:31 ;

then A7: S

for B being Element of Fin C holds S

hence G . (d,(F $$ (B,f))) = F $$ (B,(G [;] (d,f))) ; :: thesis: verum