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 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 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:23
.=
F . (F $$ ({}. C),f),
(F $$ B2,f)
by A1, A2, A4, SETWISEO:40
.=
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:23
.=
F . (F $$ B1,f),
(F $$ ({}. C),f)
by A1, A2, A4, SETWISEO:40
.=
F . (F $$ B1,f),
(F $$ B2,f)
by A6
;
verum end; hence
F $$ (B1 \/ B2),
f = F . (F $$ B1,f),
(F $$ B2,f)
;
verum 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}
by XBOOLE_0:def 7;
c in B \/ {c}
by SETWISEO:6;
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, XBOOLE_0:def 7;
now 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, Th4
.=
F . (F $$ B1,f),
(F $$ (B \/ {.c.}),f)
by A1, A15, SETWISEO:26
;
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, Th4, XBOOLE_1:7, XBOOLE_1:63
.=
F . (F $$ B1,f),
(F . (F $$ B,f),(f . c))
by A1, BINOP_1:def 3
.=
F . (F $$ B1,f),
(F $$ (B \/ {.c.}),f)
by A1, A10, A16, Th4
;
verum 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;
hence
F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)
; verum