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 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))
then consider G9 being Function of (Fin X),Y such that
A3: F $$ (B,f) = G9 . B and
for e being Element of Y st e is_a_unity_wrt F holds
G9 . {} = e and
A4: for x being Element of X holds G9 . {x} = f . x and
A5: for B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B holds
G9 . (B9 \/ {x}) = F . ((G9 . B9),(f . x)) by A1, Th13;
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
A6: 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
A7: for x being Element of X holds G . {x} = f . x and
A8: for B9 being Element of Fin X st B9 c= B \/ {x} & B9 <> {} holds
for x9 being Element of X st x9 in B \/ {x} holds
G . (B9 \/ {x9}) = F . ((G . B9),(f . x9)) by A1, Th13;
defpred S₁[ set ] means ( $1 <> {} & $1 c= B implies G . $1 = G9 . $1 );
A9: for B9 being Element of Fin X
for b being Element of X st S₁[B9] holds
S₁[B9 \/ {b}]

proof

A10: B c= B \/ {x} by XBOOLE_1:7;
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 = G9 . C ) ; :: thesis: S₁[C \/ {y}]
assume that
C \/ {y} <> {} and
A12: C \/ {y} c= B ; :: thesis: G . (C \/ {y}) = G9 . (C \/ {y})
A13: ( C c= B & y in B ) by A12, ZFMISC_1:137;

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

suppose A14: C = {} ; :: thesis: G . (C \/ {y}) = G9 . (C \/ {y})

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

end;

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

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

end;

end;

end;

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