let C, D be non empty set ; for B1, B2 being Element of Fin C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
let B1, B2 be Element of Fin C; for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
let F be BinOp of D; for f being Function of C,D st F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 holds
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
let f be Function of C,D; ( F is commutative & F is associative & ( ( B1 <> {} & B2 <> {} ) or F is having_a_unity ) & B1 misses B2 implies F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) )
assume that
A1:
( F is commutative & F is associative )
and
A2:
( ( B1 <> {} & B2 <> {} ) or F is having_a_unity )
and
A3:
B1 /\ B2 = {}
; XBOOLE_0:def 7 F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
now F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))per cases
( B1 = {} or B2 = {} or ( B1 <> {} & B2 <> {} ) )
;
suppose A4:
(
B1 = {} or
B2 = {} )
;
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))now F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))per cases
( B1 = {} or B2 = {} )
by A4;
suppose A5:
B1 = {}
;
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))hence F $$ (
(B1 \/ B2),
f) =
F . (
(the_unity_wrt F),
(F $$ (B2,f)))
by A2, SETWISEO:15
.=
F . (
(F $$ (({}. C),f)),
(F $$ (B2,f)))
by A1, A2, A4, SETWISEO:31
.=
F . (
(F $$ (B1,f)),
(F $$ (B2,f)))
by A5
;
verum end; suppose A6:
B2 = {}
;
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))hence F $$ (
(B1 \/ B2),
f) =
F . (
(F $$ (B1,f)),
(the_unity_wrt F))
by A2, SETWISEO:15
.=
F . (
(F $$ (B1,f)),
(F $$ (({}. C),f)))
by A1, A2, A4, SETWISEO:31
.=
F . (
(F $$ (B1,f)),
(F $$ (B2,f)))
by A6
;
verum end; end; end; hence
F $$ (
(B1 \/ B2),
f)
= F . (
(F $$ (B1,f)),
(F $$ (B2,f)))
;
verum end; suppose A7:
(
B1 <> {} &
B2 <> {} )
;
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))defpred S1[
Element of
Fin C]
means ( $1
<> {} &
B1 /\ $1
= {} implies
F $$ (
(B1 \/ $1),
f)
= F . (
(F $$ (B1,f)),
(F $$ ($1,f))) );
A8:
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 B be
Element of
Fin C;
for b being Element of C st S1[B] & not b in B holds
S1[B \/ {.b.}]let c be
Element of
C;
( S1[B] & not c in B implies S1[B \/ {.c.}] )
assume that A9:
(
B <> {} &
B1 /\ B = {} implies
F $$ (
(B1 \/ B),
f)
= F . (
(F $$ (B1,f)),
(F $$ (B,f))) )
and A10:
not
c in B
and
B \/ {c} <> {}
;
( not B1 /\ (B \/ {.c.}) = {} or F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f))) )
assume A11:
B1 /\ (B \/ {c}) = {}
;
F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))
then A12:
B1 misses B \/ {c}
;
c in B \/ {c}
by ZFMISC_1:136;
then A13:
not
c in B1
by A11, XBOOLE_0:def 4;
A14:
(
B <> {} &
B1 misses B implies
F $$ (
(B1 \/ B),
f)
= F . (
(F $$ (B1,f)),
(F $$ (B,f))) )
by A9;
now F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))per cases
( B = {} or B <> {} )
;
suppose A15:
B = {}
;
F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))hence F $$ (
(B1 \/ (B \/ {.c.})),
f) =
F . (
(F $$ (B1,f)),
(f . c))
by A1, A7, A13, Th2
.=
F . (
(F $$ (B1,f)),
(F $$ ((B \/ {.c.}),f)))
by A1, A15, SETWISEO:17
;
verum end; suppose A16:
B <> {}
;
F $$ ((B1 \/ (B \/ {.c.})),f) = F . ((F $$ (B1,f)),(F $$ ((B \/ {.c.}),f)))A17:
not
c in B1 \/ B
by A10, A13, XBOOLE_0:def 3;
thus F $$ (
(B1 \/ (B \/ {.c.})),
f) =
F $$ (
((B1 \/ B) \/ {.c.}),
f)
by XBOOLE_1:4
.=
F . (
(F . ((F $$ (B1,f)),(F $$ (B,f)))),
(f . c))
by A1, A14, A12, A16, A17, Th2, XBOOLE_1:7, XBOOLE_1:63
.=
F . (
(F $$ (B1,f)),
(F . ((F $$ (B,f)),(f . c))))
by A1
.=
F . (
(F $$ (B1,f)),
(F $$ ((B \/ {.c.}),f)))
by A1, A10, A16, Th2
;
verum end; end; end;
hence
F $$ (
(B1 \/ (B \/ {.c.})),
f)
= F . (
(F $$ (B1,f)),
(F $$ ((B \/ {.c.}),f)))
;
verum
end; A18:
S1[
{}. C]
;
for
B2 being
Element of
Fin C holds
S1[
B2]
from SETWISEO:sch 2(A18, A8);
hence
F $$ (
(B1 \/ B2),
f)
= F . (
(F $$ (B1,f)),
(F $$ (B2,f)))
by A3, A7;
verum end; end; end;
hence
F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))
; verum