let C, D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 = {}
; :: according to XBOOLE_0:def 7 :: thesis: 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 = {} )
;
:: thesis: F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)now per cases
( B1 = {} or B2 = {} )
by A4;
suppose A5:
B1 = {}
;
:: thesis: 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
;
:: thesis: verum end; suppose A6:
B2 = {}
;
:: thesis: 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
;
:: thesis: verum end; hence
F $$ (B1 \/ B2),
f = F . (F $$ B1,f),
(F $$ B2,f)
;
:: thesis: verum suppose A7:
(
B1 <> {} &
B2 <> {} )
;
:: thesis: 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:
S1[
{}. C]
;
A9:
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 A10:
(
B <> {} &
B1 /\ B = {} implies
F $$ (B1 \/ B),
f = F . (F $$ B1,f),
(F $$ B,f) )
and A11:
not
c in B
and
B \/ {c} <> {}
;
:: thesis: ( not B1 /\ (B \/ {.c.}) = {} or F $$ (B1 \/ (B \/ {.c.})),f = F . (F $$ B1,f),(F $$ (B \/ {.c.}),f) )
A12:
(
B <> {} &
B1 misses B implies
F $$ (B1 \/ B),
f = F . (F $$ B1,f),
(F $$ B,f) )
by A10, XBOOLE_0:def 7;
assume A13:
B1 /\ (B \/ {c}) = {}
;
:: thesis: F $$ (B1 \/ (B \/ {.c.})),f = F . (F $$ B1,f),(F $$ (B \/ {.c.}),f)
then A14:
B1 misses B \/ {c}
by XBOOLE_0:def 7;
(
c in B \/ {c} & not
c in B1 /\ (B \/ {c}) )
by A13, SETWISEO:6;
then A15:
not
c in B1
by XBOOLE_0:def 4;
now per cases
( B = {} or B <> {} )
;
suppose A16:
B = {}
;
:: thesis: 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, A15, Th4
.=
F . (F $$ B1,f),
(F $$ (B \/ {.c.}),f)
by A1, A16, SETWISEO:26
;
:: thesis: verum end; suppose A17:
B <> {}
;
:: thesis: F $$ (B1 \/ (B \/ {.c.})),f = F . (F $$ B1,f),(F $$ (B \/ {.c.}),f)then A18:
(
B1 \/ B <> {} & not
c in B1 \/ B )
by A11, A15, XBOOLE_0:def 3;
A19:
(
B c= B \/ {c} &
(B \/ {c}) /\ B1 = {} &
B1 /\ B = B /\ B1 )
by A13, XBOOLE_1:7;
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, A12, A14, A17, A18, A19, Th4, 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, A11, A17, Th4
;
:: thesis: verum end;
hence
F $$ (B1 \/ (B \/ {.c.})),
f = F . (F $$ B1,f),
(F $$ (B \/ {.c.}),f)
;
:: thesis: verum
end;
for
B2 being
Element of
Fin C holds
S1[
B2]
from SETWISEO:sch 2(A8, A9);
hence
F $$ (B1 \/ B2),
f = F . (F $$ B1,f),
(F $$ B2,f)
by A3, A7;
:: thesis: verum end;
hence
F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)
; :: thesis: verum