let f be Function of ([#] OrderedNAT),R^1; :: thesis: for seq being Function of NAT,REAL st f = seq & lim_f f <> {} holds
( seq is convergent & ex z being Real st
( z in lim_f f & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ) ) )
let seq be Function of NAT,REAL; :: thesis: ( f = seq & lim_f f <> {} implies ( seq is convergent & ex z being Real st
( z in lim_f f & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ) ) ) )
assume that
A1: f = seq and
A2: lim_f f <> {} ; :: thesis: ( seq is convergent & ex z being Real st
( z in lim_f f & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ) ) )
consider x being object such that
A3: x in lim_f f by A2, XBOOLE_0:def 1;
reconsider y = x as Point of (TopSpaceMetr RealSpace) by A3;
reconsider z = y as Real ;
A4: Balls y is basis of (BOOL2F (NeighborhoodSystem y)) by CARDFIL3:6;
consider yr being Point of RealSpace such that
A5: yr = y and
A6: Balls y = { (Ball (yr,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;
A7: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p

proof

now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p
then consider M being Nat such that
A8: not M is zero and
A9: 1 / M < p by Th5;

now :: thesis: ex i0 being Nat st
for m being Nat st i0 <= m holds
|.((seq . m) - z).| < p

Ball (yr,(1 / M)) in Balls y by A8, A6;
then consider i being Element of OrderedNAT such that
A10: for j being Element of OrderedNAT st i <= j holds
f . j in Ball (yr,(1 / M)) by A4, A3, CARDFIL2:84;
reconsider i0 = i as Nat ;
take i0 = i0; :: thesis: for m being Nat st i0 <= m holds
|.((seq . m) - z).| < p
let m be Nat; :: thesis: ( i0 <= m implies |.((seq . m) - z).| < p )
assume A11: i0 <= m ; :: thesis: |.((seq . m) - z).| < p
reconsider m0 = m as Element of OrderedNAT by ORDINAL1:def 12;
m0 in { x where x is Element of NAT : ex p0 being Element of NAT st
( i0 = p0 & p0 <= x ) } by A11;
then m0 in uparrow i by CARDFIL2:50;
then f . m0 in Ball (yr,(1 / M)) by A10, WAYBEL_0:18;
then f . m0 in ].(yr - (1 / M)),(yr + (1 / M)).[ by FRECHET:7;
then A12: ( yr - (1 / M) < seq . m0 & seq . m0 < yr + (1 / M) ) by A1, XXREAL_1:4;
( yr - p < yr - (1 / M) & yr + (1 / M) < yr + p ) by A9, XREAL_1:8, XREAL_1:15;
then ( yr - p < seq . m0 & seq . m0 < yr + p ) by A12, XXREAL_0:2;
then seq . m0 in ].(yr - p),(yr + p).[ by XXREAL_1:4;
then f . m0 in Ball (yr,p) by A1, FRECHET:7;
then f . m0 in { q where q is Element of RealSpace : dist (yr,q) < p } by METRIC_1:def 14;
then consider q0 being Element of RealSpace such that
A13: f . m0 = q0 and
A14: dist (yr,q0) < p ;
reconsider g2 = yr as Point of RealSpace ;
ex x1r, y1r being Real st
( q0 = x1r & g2 = y1r & dist (q0,g2) = real_dist . (q0,g2) & dist (q0,g2) = (Pitag_dist 1) . (<*q0*>,<*g2*>) & dist (q0,g2) = |.(x1r - y1r).| ) by Th6;
hence |.((seq . m) - z).| < p by A14, A1, A5, A13; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ; :: thesis: verum

end;

hence for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ; :: thesis: verum

end;

hence seq is convergent by SEQ_2:def 6; :: thesis: ex z being Real st
( z in lim_f f & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ) )
thus ex z being Real st
( z in lim_f f & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ) ) by A3, A7; :: thesis: verum