defpred S1[ set , set , set ] means for z being Element of F1() st z = \$2 holds
\$3 = F4(\$1,z);
A1: for n being Nat
for x being Element of F1() ex y being Element of F1() st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of F1() ex y being Element of F1() st S1[n,x,y]
let x be Element of F1(); :: thesis: ex y being Element of F1() st S1[n,x,y]
take F4(n,x) ; :: thesis: S1[n,x,F4(n,x)]
let z be Element of F1(); :: thesis: ( z = x implies F4(n,x) = F4(n,z) )
assume z = x ; :: thesis: F4(n,x) = F4(n,z)
hence F4(n,x) = F4(n,z) ; :: thesis: verum
end;
A2: for n being Nat
for x, y1, y2 being Element of F1() st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
proof
let n be Nat; :: thesis: for x, y1, y2 being Element of F1() st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2

let x, y1, y2 be Element of F1(); :: thesis: ( S1[n,x,y1] & S1[n,x,y2] implies y1 = y2 )
assume that
A3: for z being Element of F1() st z = x holds
y1 = F4(n,z) and
A4: for z being Element of F1() st z = x holds
y2 = F4(n,z) ; :: thesis: y1 = y2
thus y1 = F4(n,x) by A3
.= y2 by A4 ; :: thesis: verum
end;
A5: ( ex y being Element of F1() ex f being sequence of F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being Element of F1() st ex f being sequence of F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) & ex f being sequence of F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) ) from then consider y being Element of F1(), f being sequence of F1() such that
A6: ( y = f . F3() & f . 0 = F2() ) and
A7: for n being Nat holds S1[n,f . n,f . (n + 1)] ;
thus ex y being Element of F1() ex f being sequence of F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) :: thesis: for y1, y2 being Element of F1() st ex f being sequence of F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ex f being sequence of F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) holds
y1 = y2
proof
take y ; :: thesis: ex f being sequence of F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) )

take f ; :: thesis: ( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) )
thus ( y = f . F3() & f . 0 = F2() ) by A6; :: thesis: for n being Nat holds f . (n + 1) = F4(n,(f . n))
let n be Nat; :: thesis: f . (n + 1) = F4(n,(f . n))
reconsider n = n as Element of NAT by ORDINAL1:def 12;
S1[n,f . n,f . (n + 1)] by A7;
hence f . (n + 1) = F4(n,(f . n)) ; :: thesis: verum
end;
let y1, y2 be Element of F1(); :: thesis: ( ex f being sequence of F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ex f being sequence of F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) implies y1 = y2 )

given f being sequence of F1() such that A8: ( y1 = f . F3() & f . 0 = F2() ) and
A9: for n being Nat holds f . (n + 1) = F4(n,(f . n)) ; :: thesis: ( for f being sequence of F1() holds
( not y2 = f . F3() or not f . 0 = F2() or ex n being Nat st not f . (n + 1) = F4(n,(f . n)) ) or y1 = y2 )

A10: for n being Nat holds S1[n,f . n,f . (n + 1)] by A9;
given f2 being sequence of F1() such that A11: ( y2 = f2 . F3() & f2 . 0 = F2() ) and
A12: for n being Nat holds f2 . (n + 1) = F4(n,(f2 . n)) ; :: thesis: y1 = y2
for n being Nat holds S1[n,f2 . n,f2 . (n + 1)] by A12;
hence y1 = y2 by A5, A8, A11, A10; :: thesis: verum