let Y, X 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 & 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 );
A3: for x being Element of X holds S₁[{.x.}]

proof

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

end;

A6: 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
A8: ( ( for b being Element of X st b in B1 holds
f . b = a ) implies F $$ B1,f = a ) and
A9: ( ( for b being Element of X st b in B2 holds
f . b = a ) implies F $$ B2,f = a ) and
A10: for b being Element of X st b in B1 \/ B2 holds
f . b = a ; :: thesis: F $$ (B1 \/ B2),f = a

A11: now

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 A10; :: thesis: verum

end;

now

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 A10; :: thesis: verum

end;

hence F $$ (B1 \/ B2),f = F . a,a by A2, A8, A9, A11, Th30
.= a by A2, BINOP_1:def 4 ;
:: thesis: verum

end;

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