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 F is idempotent & F is commutative & F is associative & B <> {} holds
for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)
let F be BinOp of Y; :: thesis: for B being Element of Fin X
for f being Function of X,Y st F is idempotent & F is commutative & F is associative & B <> {} holds
for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)
let B be Element of Fin X; :: thesis: for f being Function of X,Y st F is idempotent & F is commutative & F is associative & B <> {} holds
for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)
let f be Function of X,Y; :: thesis: ( F is idempotent & F is commutative & F is associative & B <> {} implies for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x) )
assume A1: ( F is idempotent & F is commutative & F is associative ) ; :: thesis: ( not B <> {} or for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x) )
assume A2: B <> {} ; :: thesis: for x being Element of X holds F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)
let x be Element of X; :: thesis: F $$ (B \/ {.x.}),f = F . (F $$ B,f),(f . x)
consider G being Function of (Fin X),Y such that
A3: F $$ (B \/ {.x.}),f = G . (B \/ {.x.}) and
for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e and
A4: for x being Element of X holds G . {x} = f . x and
A5: for B' being Element of Fin X st B' c= B \/ {x} & B' <> {} holds
for x' being Element of X st x' in B \/ {x} holds
G . (B' \/ {x'}) = F . (G . B'),(f . x') by A1, Th25;
consider G' being Function of (Fin X),Y such that
A6: F $$ B,f = G' . B and
for e being Element of Y st e is_a_unity_wrt F holds
G' . {} = e and
A7: for x being Element of X holds G' . {x} = f . x and
A8: for B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B holds
G' . (B' \/ {x}) = F . (G' . B'),(f . x) by A1, A2, Th25;
defpred S₁[ set ] means ( $1 <> {} & $1 c= B implies G . $1 = G' . $1 );
A9: S₁[ {}. X] ;
A10: for B' being Element of Fin X
for b being Element of X st S₁[B'] holds
S₁[B' \/ {b}]

proof

let C be Element of Fin X; :: thesis: for b being Element of X st S₁[C] holds
S₁[C \/ {b}]
let y be Element of X; :: thesis: ( S₁[C] implies S₁[C \/ {y}] )
assume A11: ( C <> {} & C c= B implies G . C = G' . C ) ; :: thesis: S₁[C \/ {y}]
assume that
C \/ {y} <> {} and
A12: C \/ {y} c= B ; :: thesis: G . (C \/ {y}) = G' . (C \/ {y})
A13: ( C c= B & y in B ) by A12, Th8;
A14: B c= B \/ {x} by XBOOLE_1:7;

per cases ( C = {} or C <> {} ) ;

suppose A15: C = {} ; :: thesis: G . (C \/ {y}) = G' . (C \/ {y})

hence G . (C \/ {y}) = f . y by A4
.= G' . (C \/ {y}) by A7, A15 ;
:: thesis: verum

end;

suppose A16: C <> {} ; :: thesis: G . (C \/ {y}) = G' . (C \/ {y})

hence G . (C \/ {y}) = F . (G' . C),(f . y) by A5, A11, A13, A14, XBOOLE_1:1
.= G' . (C \/ {y}) by A8, A13, A16 ;
:: thesis: verum

end;

end;

end;

A17: for C being Element of Fin X holds S₁[C] from SETWISEO:sch 4(A9, A10);
x in B \/ {x} by Th6;
hence F $$ (B \/ {.x.}),f = F . (G . B),(f . x) by A2, A3, A5, XBOOLE_1:7
.= F . (F $$ B,f),(f . x) by A2, A6, A17 ;
:: thesis: verum