let Y, X be non empty set ; :: thesis: for F being BinOp of Y
for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds
for B1, B2 being Element of Fin X st B1 <> {} & B2 <> {} holds
F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)
let F be BinOp of Y; :: thesis: for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds
for B1, B2 being Element of Fin X st B1 <> {} & B2 <> {} holds
F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)
let f be Function of X,Y; :: thesis: ( F is idempotent & F is commutative & F is associative implies for B1, B2 being Element of Fin X st B1 <> {} & B2 <> {} holds
F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f) )
assume A1:
( F is idempotent & F is commutative & F is associative )
; :: thesis: for B1, B2 being Element of Fin X st B1 <> {} & B2 <> {} holds
F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f)
let B1, B2 be Element of Fin X; :: thesis: ( B1 <> {} & B2 <> {} implies F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f) )
assume A2:
B1 <> {}
; :: thesis: ( not B2 <> {} or F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f) )
defpred S1[ Element of Fin X] means ( $1 <> {} implies F $$ (B1 \/ $1),f = F . (F $$ B1,f),(F $$ $1,f) );
A3:
S1[ {}. X]
;
A4:
for B' being Element of Fin X
for b being Element of X st S1[B'] holds
S1[B' \/ {.b.}]
proof
let B be
Element of
Fin X;
:: thesis: for b being Element of X st S1[B] holds
S1[B \/ {.b.}]let x be
Element of
X;
:: thesis: ( S1[B] implies S1[B \/ {.x.}] )
assume that A5:
(
B <> {} implies
F $$ (B1 \/ B),
f = F . (F $$ B1,f),
(F $$ B,f) )
and
B \/ {x} <> {}
;
:: thesis: F $$ (B1 \/ (B \/ {.x.})),f = F . (F $$ B1,f),(F $$ (B \/ {.x.}),f)
per cases
( B = {} or B <> {} )
;
suppose A6:
B = {}
;
:: thesis: F $$ (B1 \/ (B \/ {.x.})),f = F . (F $$ B1,f),(F $$ (B \/ {.x.}),f)hence F $$ (B1 \/ (B \/ {.x.})),
f =
F . (F $$ B1,f),
(f . x)
by A1, A2, Th29
.=
F . (F $$ B1,f),
(F $$ (B \/ {.x.}),f)
by A1, A6, Th26
;
:: thesis: verum end; suppose A7:
B <> {}
;
:: thesis: F $$ (B1 \/ (B \/ {.x.})),f = F . (F $$ B1,f),(F $$ (B \/ {.x.}),f)thus F $$ (B1 \/ (B \/ {.x.})),
f =
F $$ ((B1 \/ B) \/ {.x.}),
f
by XBOOLE_1:4
.=
F . (F . (F $$ B1,f),(F $$ B,f)),
(f . x)
by A1, A5, A7, Th29
.=
F . (F $$ B1,f),
(F . (F $$ B,f),(f . x))
by A1, BINOP_1:def 3
.=
F . (F $$ B1,f),
(F $$ (B \/ {.x.}),f)
by A1, A7, Th29
;
:: thesis: verum end;
end;
for B2 being Element of Fin X holds S1[B2]
from SETWISEO:sch 4(A3, A4);
hence
( not B2 <> {} or F $$ (B1 \/ B2),f = F . (F $$ B1,f),(F $$ B2,f) )
; :: thesis: verum