let seq, seq1 be Real_Sequence; :: thesis: ( seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n implies seq1 is convergent )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n ; :: thesis: seq1 is convergent
consider g1 being real number such that
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p by A1, SEQ_2:def 6;
consider k being Element of NAT such that
A4: for n being Element of NAT st k <= n holds
seq1 . n = seq . n by A2;
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 ((seq1 . b₃) - g) ) )
let p be real number ; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((seq1 . b₂) - g) ) )
assume 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((seq1 . b₂) - g) )
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < p by A3;

A6: now

assume A7: n1 <= k ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - g) < p
take n = k; :: thesis: for m being Element of NAT st n <= m holds
abs ((seq1 . m) - g) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((seq1 . m) - g) < p )
assume A8: n <= m ; :: thesis: abs ((seq1 . m) - g) < p
then n1 <= m by A7, XXREAL_0:2;
then abs ((seq . m) - g1) < p by A5;
hence abs ((seq1 . m) - g) < p by A4, A8; :: thesis: verum

end;

now

assume A9: k <= n1 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - g) < p
take n = n1; :: thesis: for m being Element of NAT st n <= m holds
abs ((seq1 . m) - g) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((seq1 . m) - g) < p )
assume A10: n <= m ; :: thesis: abs ((seq1 . m) - g) < p
then seq1 . m = seq . m by A4, A9, XXREAL_0:2;
hence abs ((seq1 . m) - g) < p by A5, A10; :: thesis: verum

end;

hence ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((seq1 . b₂) - g) ) by A6; :: thesis: verum