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 . e,d = e holds
G . (F $$ B,f),d = F $$ B,(G [:] f,d)
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 . e,d = e holds
G . (F $$ B,f),d = F $$ B,(G [:] f,d)
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 . 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 )
and
A2:
F is having_a_unity
and
A3:
e = the_unity_wrt F
and
A4:
G is_distributive_wrt F
; :: thesis: ( not G . e,d = e or G . (F $$ B,f),d = F $$ B,(G [:] f,d) )
defpred S1[ Element of Fin C] means G . (F $$ $1,f),d = F $$ $1,(G [:] f,d);
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, A3, SETWISEO:40
.=
F $$ ({}. C),(G [:] f,d)
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 . (F $$ B',f),
d = F $$ B',
(G [:] f,d)
and A8:
not
c in B'
;
:: thesis: S1[B' \/ {.c.}]
thus G . (F $$ (B' \/ {.c.}),f),
d =
G . (F . (F $$ B',f),(f . c)),
d
by A1, A2, A8, Th4
.=
F . (G . (F $$ B',f),d),
(G . (f . c),d)
by A4, BINOP_1:23
.=
F . (F $$ B',(G [:] f,d)),
((G [:] f,d) . c)
by A7, FUNCOP_1:60
.=
F $$ (B' \/ {.c.}),
(G [:] f,d)
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 . (F $$ B,f),d = F $$ B,(G [:] f,d)
; :: thesis: verum