let C, D be non empty set ; 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; 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; 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; 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; ( 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
; ( 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)));
A4:
for B9 being Element of Fin C
for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]
proof
let B9 be
Element of
Fin C;
for b being Element of C st S1[B9] & not b in B9 holds
S1[B9 \/ {.b.}]let c be
Element of
C;
( S1[B9] & not c in B9 implies S1[B9 \/ {.c.}] )
assume that A5:
G . (
(F $$ (B9,f)),
d)
= F $$ (
B9,
(G [:] (f,d)))
and A6:
not
c in B9
;
S1[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
;
verum
end;
assume
G . (e,d) = e
; 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:
S1[ {}. C]
;
for B being Element of Fin C holds S1[B]
from SETWISEO:sch 2(A7, A4);
hence
G . ((F $$ (B,f)),d) = F $$ (B,(G [:] (f,d)))
; verum