let X, Y be non empty set ; :: thesis: for F being BinOp of Y
for B being Element of Fin X
for f being Function of X,Y st B <> {} & F is commutative & F is associative & F is idempotent holds
for a being Element of Y st ( for b being Element of X st b in B holds
f . b = a ) holds
F $$ (B,f) = a
let F be BinOp of Y; :: thesis: for B being Element of Fin X
for f being Function of X,Y st B <> {} & F is commutative & F is associative & F is idempotent holds
for a being Element of Y st ( for b being Element of X st b in B holds
f . b = a ) holds
F $$ (B,f) = a
let B be Element of Fin X; :: thesis: for f being Function of X,Y st B <> {} & F is commutative & F is associative & F is idempotent holds
for a being Element of Y st ( for b being Element of X st b in B holds
f . b = a ) holds
F $$ (B,f) = a
let f be Function of X,Y; :: thesis: ( B <> {} & F is commutative & F is associative & F is idempotent implies for a being Element of Y st ( for b being Element of X st b in B holds
f . b = a ) holds
F $$ (B,f) = a )
assume that
A1: B <> {} and
A2: ( F is commutative & F is associative ) and
A3: F is idempotent ; :: thesis: for a being Element of Y st ( for b being Element of X st b in B holds
f . b = a ) holds
F $$ (B,f) = a
let a be Element of Y; :: thesis: ( ( for b being Element of X st b in B holds
f . b = a ) implies F $$ (B,f) = a )
defpred S₁[ Element of Fin X] means ( ( for b being Element of X st b in $1 holds
f . b = a ) implies F $$ ($1,f) = a );
A4: for B1, B2 being non empty Element of Fin X st S₁[B1] & S₁[B2] holds
S₁[B1 \/ B2]

proof

let B1, B2 be non empty Element of Fin X; :: thesis: ( S₁[B1] & S₁[B2] implies S₁[B1 \/ B2] )
assume that
A5: ( ( ( for b being Element of X st b in B1 holds
f . b = a ) implies F $$ (B1,f) = a ) & ( ( for b being Element of X st b in B2 holds
f . b = a ) implies F $$ (B2,f) = a ) ) and
A6: for b being Element of X st b in B1 \/ B2 holds
f . b = a ; :: thesis: F $$ ((B1 \/ B2),f) = a

A7: now :: thesis: for b being Element of X st b in B2 holds
f . b = a

let b be Element of X; :: thesis: ( b in B2 implies f . b = a )
assume b in B2 ; :: thesis: f . b = a
then b in B1 \/ B2 by XBOOLE_0:def 3;
hence f . b = a by A6; :: thesis: verum

end;

now :: thesis: for b being Element of X st b in B1 holds
f . b = a

let b be Element of X; :: thesis: ( b in B1 implies f . b = a )
assume b in B1 ; :: thesis: f . b = a
then b in B1 \/ B2 by XBOOLE_0:def 3;
hence f . b = a by A6; :: thesis: verum

end;

hence F $$ ((B1 \/ B2),f) = F . (a,a) by A2, A3, A5, A7, Th18
.= a by A3 ;
:: thesis: verum

end;

A8: for x being Element of X holds S₁[{.x.}]

proof

let x be Element of X; :: thesis: S₁[{.x.}]
assume A9: for b being Element of X st b in {x} holds
f . b = a ; :: thesis: F $$ ({.x.},f) = a
A10: x in {x} by TARSKI:def 1;
thus F $$ ({.x.},f) = f . x by A2, Th14
.= a by A9, A10 ; :: thesis: verum

end;

for B being non empty Element of Fin X holds S₁[B] from SETWISEO:sch 3(A8, A4);
hence ( ( for b being Element of X st b in B holds
f . b = a ) implies F $$ (B,f) = a ) by A1; :: thesis: verum