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:215;
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 n <= m ; :: thesis: abs ((seq . m) - (seq . n)) < s
then A3: abs ((seq . m) - g1) < s / 2 by A2;
A4: abs (((seq . m) - g1) + (g1 - (seq . n))) <= (abs ((seq . m) - g1)) + (abs (g1 - (seq . n))) by COMPLEX1:56;
abs ((seq . n) - g1) < s / 2 by A2;
then abs (- (g1 - (seq . n))) < s / 2 ;
then abs (g1 - (seq . n)) < s / 2 by COMPLEX1:52;
then (abs ((seq . m) - g1)) + (abs (g1 - (seq . n))) < (s / 2) + (s / 2) by A3, XREAL_1:8;
hence abs ((seq . m) - (seq . n)) < s by A4, XXREAL_0:2; :: thesis: verum

end;

assume A5: 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
A6: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (seq . n1)) < 1 ;
consider r1 being real number such that
A7: 0 < r1 and
A8: for m being Element of NAT st m <= n1 holds
abs (seq . m) < r1 by SEQ_2:4;

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 A7, COMPLEX1:46, XREAL_1:8;
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

A9: now

assume n1 <= m ; :: thesis: abs (seq . m) < r
then A10: abs ((seq . m) - (seq . n1)) < 1 by A6;
(abs (seq . m)) - (abs (seq . n1)) <= abs ((seq . m) - (seq . n1)) by COMPLEX1:59;
then (abs (seq . m)) - (abs (seq . n1)) < 1 by A10, XXREAL_0:2;
then ((abs (seq . m)) - (abs (seq . n1))) + (abs (seq . n1)) < 1 + (abs (seq . n1)) by XREAL_1:6;
then 0 + (abs (seq . m)) < r1 + ((abs (seq . n1)) + 1) by A7, XREAL_1:8;
hence abs (seq . m) < r ; :: thesis: verum

end;

now

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

end;

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

end;

then seq is bounded by SEQ_2:3;
then consider seq1 being Real_Sequence such that
A11: seq1 is subsequence of seq and
A12: seq1 is convergent by Th57;
consider g1 being real number such that
A13: 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 A12, SEQ_2:def 6;
take 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₃) - g1) ) )
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₂) - g1) ) )
assume A14: 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₂) - g1) )
then consider n1 being Element of NAT such that
A15: for m being Element of NAT st n1 <= m holds
abs ((seq1 . m) - g1) < s / 3 by A13, XREAL_1:222;
consider n2 being Element of NAT such that
A16: for m being Element of NAT st n2 <= m holds
abs ((seq . m) - (seq . n2)) < s / 3 by A5, A14, XREAL_1:222;
take n = n1 + n2; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not s <= abs ((seq . b₁) - g1) )
let m be Element of NAT ; :: thesis: ( not n <= m or not s <= abs ((seq . m) - g1) )
assume A17: n <= m ; :: thesis: not s <= abs ((seq . m) - g1)
consider Nseq being V35() sequence of NAT such that
A18: seq1 = seq * Nseq by A11, VALUED_0:def 17;
n1 <= n by NAT_1:12;
then n1 <= m by A17, XXREAL_0:2;
then abs (((seq * Nseq) . m) - g1) < s / 3 by A18, A15;
then A19: abs ((seq . (Nseq . m)) - g1) < s / 3 by FUNCT_2:15;
n2 <= n by NAT_1:12;
then A20: n2 <= m by A17, XXREAL_0:2;
m <= Nseq . m by SEQM_3:14;
then n2 <= Nseq . m by A20, XXREAL_0:2;
then abs ((seq . (Nseq . m)) - (seq . n2)) < s / 3 by A16;
then abs (- ((seq . n2) - (seq . (Nseq . m)))) < s / 3 ;
then A21: abs ((seq . n2) - (seq . (Nseq . m))) < s / 3 by COMPLEX1:52;
abs ((seq . m) - (seq . n2)) < s / 3 by A16, A20;
then A22: (abs ((seq . m) - (seq . n2))) + (abs ((seq . n2) - (seq . (Nseq . m)))) < (s / 3) + (s / 3) by A21, XREAL_1:8;
abs (((seq . m) - (seq . n2)) + ((seq . n2) - (seq . (Nseq . m)))) <= (abs ((seq . m) - (seq . n2))) + (abs ((seq . n2) - (seq . (Nseq . m)))) by COMPLEX1:56;
then abs ((seq . m) - (seq . (Nseq . m))) < (s / 3) + (s / 3) by A22, XXREAL_0:2;
then A23: (abs ((seq . m) - (seq . (Nseq . m)))) + (abs ((seq . (Nseq . m)) - g1)) < ((s / 3) + (s / 3)) + (s / 3) by A19, XREAL_1:8;
abs (((seq . m) - (seq . (Nseq . m))) + ((seq . (Nseq . m)) - g1)) <= (abs ((seq . m) - (seq . (Nseq . m)))) + (abs ((seq . (Nseq . m)) - g1)) by COMPLEX1:56;
hence not s <= abs ((seq . m) - g1) by A23, XXREAL_0:2; :: thesis: verum