let seq be Real_Sequence; :: thesis: ( seq is convergent iff for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s )
thus ( seq is convergent implies for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s ) :: thesis: ( ( for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s ) implies seq is convergent )

proof

assume seq is convergent ; :: thesis: for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s
then consider g1 being real number such that
A1: for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < s by SEQ_2:def 6;
let s be real number ; :: thesis: ( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s )
assume 0 < s ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s
then consider n1 being Element of NAT such that
A2: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < s / 2 by A1, XREAL_1:217;
take n = n1; :: thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((seq . m) - (seq . n)) < s )
assume A3: n <= m ; :: thesis: abs ((seq . m) - (seq . n)) < s
abs ((seq . n) - g1) < s / 2 by A2;
then abs (- (g1 - (seq . n))) < s / 2 ;
then A4: abs (g1 - (seq . n)) < s / 2 by COMPLEX1:138;
abs ((seq . m) - g1) < s / 2 by A2, A3;
then A5: (abs ((seq . m) - g1)) + (abs (g1 - (seq . n))) < (s / 2) + (s / 2) by A4, XREAL_1:10;
abs (((seq . m) - g1) + (g1 - (seq . n))) <= (abs ((seq . m) - g1)) + (abs (g1 - (seq . n))) by COMPLEX1:142;
hence abs ((seq . m) - (seq . n)) < s by A5, XXREAL_0:2; :: thesis: verum

end;

assume A6: for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s ; :: thesis: seq is convergent
then consider n1 being Element of NAT such that
A7: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (seq . n1)) < 1 ;
consider r1 being real number such that
A8: 0 < r1 and
A9: for m being Element of NAT st m <= n1 holds
abs (seq . m) < r1 by SEQ_2:16;

now

take r = (r1 + (abs (seq . n1))) + 1; :: thesis: ( 0 < r & ( for m being Element of NAT holds abs (seq . m) < r ) )
0 + 0 < r1 + (abs (seq . n1)) by A8, COMPLEX1:132, XREAL_1:10;
hence 0 < r ; :: thesis: for m being Element of NAT holds abs (seq . m) < r
let m be Element of NAT ; :: thesis: abs (seq . m) < r

A10: now

assume m <= n1 ; :: thesis: abs (seq . m) < r
then abs (seq . m) < r1 by A9;
then (abs (seq . m)) + 0 < r1 + (abs (seq . n1)) by COMPLEX1:132, XREAL_1:10;
hence abs (seq . m) < r by XREAL_1:10; :: thesis: verum

end;

now

assume n1 <= m ; :: thesis: abs (seq . m) < r
then A11: abs ((seq . m) - (seq . n1)) < 1 by A7;
(abs (seq . m)) - (abs (seq . n1)) <= abs ((seq . m) - (seq . n1)) by COMPLEX1:145;
then (abs (seq . m)) - (abs (seq . n1)) < 1 by A11, XXREAL_0:2;
then ((abs (seq . m)) - (abs (seq . n1))) + (abs (seq . n1)) < 1 + (abs (seq . n1)) by XREAL_1:8;
then 0 + (abs (seq . m)) < r1 + ((abs (seq . n1)) + 1) by A8, XREAL_1:10;
hence abs (seq . m) < r ; :: thesis: verum

end;

hence abs (seq . m) < r by A10; :: thesis: verum

end;

then seq is bounded by SEQ_2:15;
then consider seq1 being Real_Sequence such that
A12: seq1 is subsequence of seq and
A13: seq1 is convergent by Th57;
consider g1 being real number such that
A14: for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - g1) < s by A13, SEQ_2:def 6;
consider Nseq being V33() sequence of NAT such that
A15: seq1 = seq * Nseq by A12, VALUED_0:def 17;
take g = g1; :: according to SEQ_2:def 6 :: thesis: for b₁ being set holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= abs ((seq . b₃) - g) ) )
let s be real number ; :: thesis: ( s <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not s <= abs ((seq . b₂) - g) ) )
assume Z: 0 < s ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not s <= abs ((seq . b₂) - g) )
then consider n1 being Element of NAT such that
A17: for m being Element of NAT st n1 <= m holds
abs ((seq1 . m) - g1) < s / 3 by A14, XREAL_1:224;
consider n2 being Element of NAT such that
A18: for m being Element of NAT st n2 <= m holds
abs ((seq . m) - (seq . n2)) < s / 3 by A6, Z, XREAL_1:224;
take n = n1 + n2; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not s <= abs ((seq . b₁) - g) )
let m be Element of NAT ; :: thesis: ( not n <= m or not s <= abs ((seq . m) - g) )
assume A19: n <= m ; :: thesis: not s <= abs ((seq . m) - g)
n1 <= n by NAT_1:12;
then n1 <= m by A19, XXREAL_0:2;
then abs (((seq * Nseq) . m) - g1) < s / 3 by A15, A17;
then A20: abs ((seq . (Nseq . m)) - g1) < s / 3 by FUNCT_2:21;
n2 <= n by NAT_1:12;
then A21: n2 <= m by A19, XXREAL_0:2;
then A22: abs ((seq . m) - (seq . n2)) < s / 3 by A18;
m <= Nseq . m by SEQM_3:33;
then n2 <= Nseq . m by A21, XXREAL_0:2;
then abs ((seq . (Nseq . m)) - (seq . n2)) < s / 3 by A18;
then abs (- ((seq . n2) - (seq . (Nseq . m)))) < s / 3 ;
then abs ((seq . n2) - (seq . (Nseq . m))) < s / 3 by COMPLEX1:138;
then A23: (abs ((seq . m) - (seq . n2))) + (abs ((seq . n2) - (seq . (Nseq . m)))) < (s / 3) + (s / 3) by A22, XREAL_1:10;
abs (((seq . m) - (seq . n2)) + ((seq . n2) - (seq . (Nseq . m)))) <= (abs ((seq . m) - (seq . n2))) + (abs ((seq . n2) - (seq . (Nseq . m)))) by COMPLEX1:142;
then abs ((seq . m) - (seq . (Nseq . m))) < (s / 3) + (s / 3) by A23, XXREAL_0:2;
then A24: (abs ((seq . m) - (seq . (Nseq . m)))) + (abs ((seq . (Nseq . m)) - g1)) < ((s / 3) + (s / 3)) + (s / 3) by A20, XREAL_1:10;
abs (((seq . m) - (seq . (Nseq . m))) + ((seq . (Nseq . m)) - g1)) <= (abs ((seq . m) - (seq . (Nseq . m)))) + (abs ((seq . (Nseq . m)) - g1)) by COMPLEX1:142;
hence not s <= abs ((seq . m) - g) by A24, XXREAL_0:2; :: thesis: verum