let r be real number ; :: thesis: for seq being Real_Sequence st ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m = r holds
( seq is convergent & lim seq = r )
let seq be Real_Sequence; :: thesis: ( ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m = r implies ( seq is convergent & lim seq = r ) )
assume A1: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m = r ; :: thesis: ( seq is convergent & lim seq = r )
A2: for r1 being real number st 0 < r1 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < r1

proof

let r1 be real number ; :: thesis: ( 0 < r1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < r1 )
assume A3: 0 < r1 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < r1
consider n being Element of NAT such that
A4: for m being Element of NAT st n <= m holds
seq . m = r by A1;
take n ; :: thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < r1
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((seq . m) - r) < r1 )
assume n <= m ; :: thesis: abs ((seq . m) - r) < r1
then seq . m = r by A4;
hence abs ((seq . m) - r) < r1 by A3, ABSVALUE:7; :: thesis: verum

end;

then seq is convergent by SEQ_2:def 6;
hence ( seq is convergent & lim seq = r ) by A2, SEQ_2:def 7; :: thesis: verum