let X, Y 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 that
A1: F is idempotent and
A2: F is commutative and
A3: 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))) )
defpred S₁[ Element of Fin X] means ( $1 <> {} implies F $$ ((B1 \/ $1),f) = F . ((F $$ (B1,f)),(F $$ ($1,f))) );
assume A4: B1 <> {} ; :: thesis: ( not B2 <> {} or F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) )
A5: for B9 being Element of Fin X
for b being Element of X st S₁[B9] holds
S₁[B9 \/ {.b.}]

proof

let B be Element of Fin X; :: thesis: for b being Element of X st S₁[B] holds
S₁[B \/ {.b.}]
let x be Element of X; :: thesis: ( S₁[B] implies S₁[B \/ {.x.}] )
assume that
A6: ( 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 A7: 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, A3, A4, Th17
.= F . ((F $$ (B1,f)),(F $$ ((B \/ {.x.}),f))) by A2, A3, A7, Th14 ;
:: thesis: verum

end;

suppose A8: 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, A2, A3, A6, A8, Th17
.= F . ((F $$ (B1,f)),(F . ((F $$ (B,f)),(f . x)))) by A3
.= F . ((F $$ (B1,f)),(F $$ ((B \/ {.x.}),f))) by A1, A2, A3, A8, Th17 ; :: thesis: verum

end;

end;

end;

A9: S₁[ {}. X] ;
for B2 being Element of Fin X holds S₁[B2] from SETWISEO:sch 4(A9, A5);
hence ( not B2 <> {} or F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f))) ) ; :: thesis: verum