let C, D be non empty set ; :: thesis: for B being Element of Fin C
for e, d 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 e, d 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 e, d 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 )
and
A2:
F is having_a_unity
and
A3:
e = the_unity_wrt F
and
A4:
G is_distributive_wrt F
; :: thesis: ( not G . d,e = e or G . d,(F $$ B,f) = F $$ B,(G [;] d,f) )
defpred S1[ Element of Fin C] means G . d,(F $$ $1,f) = F $$ $1,(G [;] d,f);
assume
G . d,e = e
; :: thesis: G . d,(F $$ B,f) = F $$ B,(G [;] d,f)
then G . d,(F $$ ({}. C),f) =
e
by A1, A2, A3, SETWISEO:40
.=
F $$ ({}. C),(G [;] d,f)
by A1, A2, A3, SETWISEO:40
;
then A5:
S1[ {}. C]
;
A6:
for B' being Element of Fin C
for b being Element of C st S1[B'] & not b in B' holds
S1[B' \/ {.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 A7:
G . d,
(F $$ B',f) = F $$ B',
(G [;] d,f)
and A8:
not
c in B'
;
:: thesis: S1[B' \/ {.c.}]
thus G . d,
(F $$ (B' \/ {.c.}),f) =
G . d,
(F . (F $$ B',f),(f . c))
by A1, A2, A8, Th4
.=
F . (G . d,(F $$ B',f)),
(G . d,(f . c))
by A4, BINOP_1:23
.=
F . (F $$ B',(G [;] d,f)),
((G [;] d,f) . c)
by A7, FUNCOP_1:66
.=
F $$ (B' \/ {.c.}),
(G [;] d,f)
by A1, A2, A8, Th4
;
:: thesis: verum
end;
for B being Element of Fin C holds S1[B]
from SETWISEO:sch 2(A5, A6);
hence
G . d,(F $$ B,f) = F $$ B,(G [;] d,f)
; :: thesis: verum