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 ) 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

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

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, Th30
.= a by A3, BINOP_1:def 4 ;
:: 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, Th26
.= 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