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

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

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

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

end;

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

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

proof

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

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

suppose A71: B9 = {} ; :: thesis: G1 . (B9 \/ {x}) = G2 . (B9 \/ {x})

hence G1 . (B9 \/ {x}) = f . x by A56
.= G2 . (B9 \/ {x}) by A60, A71 ;
:: thesis: verum

end;

suppose A72: B9 <> {} ; :: thesis: G1 . (B9 \/ {x}) = G2 . (B9 \/ {x})

hence G1 . (B9 \/ {x}) = F . (G1 . B9),(f . x) by A57, A69, A70
.= G2 . (B9 \/ {x}) by A61, A66, A69, A70, A72 ;
:: thesis: verum

end;

end;

end;

A73: S₁[ {}. X] ;
for B9 being Element of Fin X holds S₁[B9] from SETWISEO:sch 2(A73, A65);
hence x = y by A54, A58, A64; :: thesis: verum

end;

end;