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

( 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

( 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

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 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

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

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;

for m being Nat st n <= m holds

|.((seq . m) - z).| < p ; :: thesis: verum

end;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

hence
ex n 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;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

for m being Nat st n <= m holds

|.((seq . m) - z).| < p ; :: thesis: verum

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - z).| < p ; :: thesis: verum

( 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