let C, D be non empty set ; :: thesis: for B being Element of Fin C
for e being Element of D
for F, G being BinOp of D
for f, f' being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . e,e = e & ( for d1, d2, d3, d4 being Element of D holds F . (G . d1,d2),(G . d3,d4) = G . (F . d1,d3),(F . d2,d4) ) holds
G . (F $$ B,f),(F $$ B,f') = F $$ B,(G .: f,f')
let B be Element of Fin C; :: thesis: for e being Element of D
for F, G being BinOp of D
for f, f' being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . e,e = e & ( for d1, d2, d3, d4 being Element of D holds F . (G . d1,d2),(G . d3,d4) = G . (F . d1,d3),(F . d2,d4) ) holds
G . (F $$ B,f),(F $$ B,f') = F $$ B,(G .: f,f')
let e be Element of D; :: thesis: for F, G being BinOp of D
for f, f' being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . e,e = e & ( for d1, d2, d3, d4 being Element of D holds F . (G . d1,d2),(G . d3,d4) = G . (F . d1,d3),(F . d2,d4) ) holds
G . (F $$ B,f),(F $$ B,f') = F $$ B,(G .: f,f')
let F, G be BinOp of D; :: thesis: for f, f' being Function of C,D st F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . e,e = e & ( for d1, d2, d3, d4 being Element of D holds F . (G . d1,d2),(G . d3,d4) = G . (F . d1,d3),(F . d2,d4) ) holds
G . (F $$ B,f),(F $$ B,f') = F $$ B,(G .: f,f')
let f, f' be Function of C,D; :: thesis: ( F is commutative & F is associative & F is having_a_unity & e = the_unity_wrt F & G . e,e = e & ( for d1, d2, d3, d4 being Element of D holds F . (G . d1,d2),(G . d3,d4) = G . (F . d1,d3),(F . d2,d4) ) implies G . (F $$ B,f),(F $$ B,f') = F $$ B,(G .: f,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 . e,e = e
and
A5:
for d1, d2, d3, d4 being Element of D holds F . (G . d1,d2),(G . d3,d4) = G . (F . d1,d3),(F . d2,d4)
; :: thesis: G . (F $$ B,f),(F $$ B,f') = F $$ B,(G .: f,f')
defpred S1[ Element of Fin C] means G . (F $$ $1,f),(F $$ $1,f') = F $$ $1,(G .: f,f');
( F $$ ({}. C),f = e & F $$ ({}. C),f' = e )
by A1, A2, A3, SETWISEO:40;
then A6:
S1[ {}. C]
by A1, A2, A3, A4, SETWISEO:40;
A7:
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 A8:
G . (F $$ B,f),
(F $$ B,f') = F $$ B,
(G .: f,f')
and A9:
not
c in B
;
:: thesis: S1[B \/ {.c.}]
set s =
F $$ B,
f;
set s' =
F $$ B,
f';
(
F $$ (B \/ {.c.}),
f = F . (F $$ B,f),
(f . c) &
F $$ (B \/ {.c.}),
f' = F . (F $$ B,f'),
(f' . c) )
by A1, A2, A9, Th4;
hence G . (F $$ (B \/ {.c.}),f),
(F $$ (B \/ {.c.}),f') =
F . (G . (F $$ B,f),(F $$ B,f')),
(G . (f . c),(f' . c))
by A5
.=
F . (G . (F $$ B,f),(F $$ B,f')),
((G .: f,f') . c)
by FUNCOP_1:48
.=
F $$ (B \/ {.c.}),
(G .: f,f')
by A1, A2, A8, A9, Th4
;
:: thesis: verum
end;
for B being Element of Fin C holds S1[B]
from SETWISEO:sch 2(A6, A7);
hence
G . (F $$ B,f),(F $$ B,f') = F $$ B,(G .: f,f')
; :: thesis: verum