let x, y be Element of Y; :: thesis: ( ex G being Function of (Fin X),Y st
( x = 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 \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) ) & ex G being Function of (Fin X),Y st
( y = 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 \ B' holds
G . (B' \/ {x}) = F . (G . B'),(f . x) ) ) implies x = y )
given G1 being Function of (Fin X),Y such that A50: x = G1 . B and
A51: for e being Element of Y st e is_a_unity_wrt F holds
G1 . {} = e and
A52: for x being Element of X holds G1 . {x} = f . x and
A53: 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
G1 . (B' \/ {x}) = F . (G1 . B'),(f . x) ; :: thesis: ( for G being Function of (Fin X),Y holds
( not y = G . B or ex e being Element of Y st
( e is_a_unity_wrt F & not G . {} = e ) or ex x being Element of X st not G . {x} = f . x or ex B' being Element of Fin X st
( B' c= B & B' <> {} & ex x being Element of X st
( x in B \ B' & not G . (B' \/ {x}) = F . (G . B'),(f . x) ) ) ) or x = y )
given G2 being Function of (Fin X),Y such that A54: y = G2 . B and
A55: for e being Element of Y st e is_a_unity_wrt F holds
G2 . {} = e and
A56: for x being Element of X holds G2 . {x} = f . x and
A57: 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
G2 . (B' \/ {x}) = F . (G2 . B'),(f . x) ; :: thesis: x = y

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

suppose A58: B = {} ; :: thesis: x = y

then A59: the_unity_wrt F is_a_unity_wrt F by A1, Th22;
hence x = the_unity_wrt F by A50, A51, A58
.= y by A54, A55, A58, A59 ;
:: thesis: verum

end;

suppose A60: B <> {} ; :: thesis: x = y

defpred S₁[ set ] means ( $1 c= B & $1 <> {} implies G1 . $1 = G2 . $1 );
A61: S₁[ {}. X] ;
A62: for B' being Element of Fin X
for b being Element of X st S₁[B'] & not b in B' holds
S₁[B' \/ {b}]

proof

let B' be Element of Fin X; :: thesis: for b being Element of X st S₁[B'] & not b in B' holds
S₁[B' \/ {b}]
let x be Element of X; :: thesis: ( S₁[B'] & not x in B' implies S₁[B' \/ {x}] )
assume A63: ( B' c= B & B' <> {} implies G1 . B' = G2 . B' ) ; :: thesis: ( x in B' or S₁[B' \/ {x}] )
assume A64: not x in B' ; :: thesis: S₁[B' \/ {x}]
assume B' \/ {x} c= B ; :: thesis: ( not B' \/ {x} <> {} or G1 . (B' \/ {x}) = G2 . (B' \/ {x}) )
then A65: ( B' c= B & x in B ) by Th8;
then A66: x in B \ B' by A64, XBOOLE_0:def 5;
assume B' \/ {x} <> {} ; :: thesis: G1 . (B' \/ {x}) = G2 . (B' \/ {x})

per cases ( B' = {} or B' <> {} ) ;

suppose A67: B' = {} ; :: thesis: G1 . (B' \/ {x}) = G2 . (B' \/ {x})

hence G1 . (B' \/ {x}) = f . x by A52
.= G2 . (B' \/ {x}) by A56, A67 ;
:: thesis: verum

end;

suppose A68: B' <> {} ; :: thesis: G1 . (B' \/ {x}) = G2 . (B' \/ {x})

hence G1 . (B' \/ {x}) = F . (G1 . B'),(f . x) by A53, A65, A66
.= G2 . (B' \/ {x}) by A57, A63, A65, A66, A68 ;
:: thesis: verum

end;

end;

end;

for B' being Element of Fin X holds S₁[B'] from SETWISEO:sch 2(A61, A62);
hence x = y by A50, A54, A60; :: thesis: verum

end;

end;