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 ( B <> {} or F is having_a_unity ) & F is idempotent & F is commutative & F is associative holds
for IT being Element of Y holds
( IT = F $$ (B,f) iff 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) )
let F be BinOp of Y; :: thesis: for B being Element of Fin X
for f being Function of X,Y st ( B <> {} or F is having_a_unity ) & F is idempotent & F is commutative & F is associative holds
for IT being Element of Y holds
( IT = F $$ (B,f) iff 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) )
let B be Element of Fin X; :: thesis: for f being Function of X,Y st ( B <> {} or F is having_a_unity ) & F is idempotent & F is commutative & F is associative holds
for IT being Element of Y holds
( IT = F $$ (B,f) iff 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) )
let f be Function of X,Y; :: thesis: ( ( B <> {} or F is having_a_unity ) & F is idempotent & F is commutative & F is associative implies for IT being Element of Y holds
( IT = F $$ (B,f) iff 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) )
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: for IT being Element of Y holds
( IT = F $$ (B,f) iff 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) )
let IT be Element of Y; :: thesis: ( IT = F $$ (B,f) iff 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) )
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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) :: thesis: ( 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) implies IT = F $$ (B,f) )

proof

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

proof

let B9 be Element of Fin X; :: thesis: ( B9 c= B & B9 <> {} implies for x being Element of X st x in B holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) )
assume that
A8: B9 c= B and
A9: B9 <> {} ; :: thesis: for x being Element of X st x in B holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x))
let x be Element of X; :: thesis: ( x in B implies G . (B9 \/ {x}) = F . ((G . B9),(f . x)) )
assume A10: x in B ; :: thesis: G . (B9 \/ {x}) = F . ((G . B9),(f . x))

per cases ( x in B9 or not x in B9 ) ;

suppose x in B9 ; :: thesis: G . (B9 \/ {x}) = F . ((G . B9),(f . x))

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

per cases ( B9 = {x} or B9 <> {x} ) ;

suppose A14: B9 = {x} ; :: thesis: G . (B9 \/ {x}) = F . ((G . B9),(f . x))

hence G . (B9 \/ {x}) = F . ((f . x),(f . x)) by A2, A6
.= F . ((G . B9),(f . x)) by A6, A14 ;
:: thesis: verum

end;

suppose B9 <> {x} ; :: thesis: G . (B9 \/ {x}) = F . ((G . B9),(f . x))

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

end;

end;

end;

suppose not x in B9 ; :: thesis: G . (B9 \/ {x}) = F . ((G . B9),(f . x))

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

end;

end;

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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds
for x being Element of X st x in B holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) by A5, A6; :: thesis: verum

end;

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

proof

let B9 be Element of Fin X; :: thesis: ( B9 c= B & B9 <> {} implies for x being Element of X st x in B \ B9 holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) )
assume A18: ( B9 c= B & B9 <> {} ) ; :: thesis: for x being Element of X st x in B \ B9 holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x))
let x be Element of X; :: thesis: ( x in B \ B9 implies G . (B9 \/ {x}) = F . ((G . B9),(f . x)) )
assume x in B \ B9 ; :: thesis: G . (B9 \/ {x}) = F . ((G . B9),(f . x))
then x in B by XBOOLE_0:def 5;
hence G . (B9 \/ {x}) = F . ((G . B9),(f . x)) by A17, A18; :: thesis: verum

end;

hence IT = F $$ (B,f) by A1, A3, A4, A16, Def3; :: thesis: verum