let X, Y be non empty set ; :: thesis:
let F be BinOp of Y; :: thesis:
let B be Element of Fin X; :: thesis:
let f be Function of X,Y; :: thesis:
assume that
A1: ( B <> {} or F is having_a_unity ) and
A2: F is idempotent and
A3: F is commutative and
A4: F is associative ; :: thesis:
let IT be Element of Y; :: thesis:
thus ( IT = F $$ B,f implies ex G being Function of (Fin X),Y st
( IT = G . B & ( for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( 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) ) ) ) :: thesis:

proof

assume IT = F $$ B,f ; :: thesis:
then consider G being Function of (Fin X),Y such that
A5: IT = G . B and
A6: 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 \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) by A1, A3, A4, Def3;
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)

proof

let B' be Element of Fin X; :: thesis:
assume A9: ( B' c= B & B' <> {} ) ; :: thesis:
let x be Element of X; :: thesis:
assume A10: x in B ; :: thesis:

per cases ;

suppose x in B' ; :: thesis:

then A11: B' \/ {x} = B' by ZFMISC_1:46;
then A12: {x} c= B' by XBOOLE_1:7;
not x in B' \ {x} by ZFMISC_1:64;
then A13: x in B \ (B' \ {x}) by A10, XBOOLE_0:def 5;

per cases ;

suppose A14: B' = {x} ; :: thesis:

hence G . (B' \/ {x}) = f . x by A7
.= F . (f . x),(f . x) by A2, BINOP_1:def 4
.= F . (G . B'),(f . x) by A7, A14 ;
:: thesis:

end;

suppose B' <> {x} ; :: thesis:

then not B' c= {x} by A12, XBOOLE_0:def 10;
then B' \ {x} <> {} by XBOOLE_1:37;
then A15: G . ((B' \ {.x.}) \/ {.x.}) = F . (G . (B' \ {.x.})),(f . x) by A8, A9, A13, XBOOLE_1:1;
thus G . (B' \/ {x}) = G . ((B' \ {x}) \/ {x}) by XBOOLE_1:39
.= F . (G . (B' \ {x})),(F . (f . x),(f . x)) by A2, A15, BINOP_1:def 4
.= F . (F . (G . (B' \ {.x.})),(f . x)),(f . x) by A4, BINOP_1:def 3
.= F . (G . B'),(f . x) by A11, A15, XBOOLE_1:39 ; :: thesis:

end;

suppose not x in B' ; :: thesis:

then x in B \ B' by A10, XBOOLE_0:def 5;
hence G . (B' \/ {x}) = F . (G . B'),(f . x) by A8, A9; :: thesis:

end;

hence ex G being Function of (Fin X),Y st
( IT = G . B & ( for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e ) & ( for x being Element of X holds G . {x} = f . x ) & ( 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 A5, A6, A7; :: thesis:

end;

given G being Function of (Fin X),Y such that A16: IT = G . B and
A17: for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e and
A18: for x being Element of X holds G . {x} = f . x and
A19: 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) ; :: thesis:
for B' being Element of Fin X st B' c= B & B' <> {} holds
for x being Element of X st x in B \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x)

proof

let B' be Element of Fin X; :: thesis:
assume A20: ( B' c= B & B' <> {} ) ; :: thesis:
let x be Element of X; :: thesis:
assume x in B \ B' ; :: thesis:
then x in B by XBOOLE_0:def 5;
hence G . (B' \/ {x}) = F . (G . B'),(f . x) by A19, A20; :: thesis:

end;

hence IT = F $$ B,f by A1, A3, A4, A16, A17, A18, Def3; :: thesis: