let r be Real; :: thesis: for seq being Real_Sequence st ex n being Nat st
for m being Nat st n <= m holds
seq . m = r holds
( seq is convergent & lim seq = r )
let seq be Real_Sequence; :: thesis: ( ex n being Nat st
for m being Nat st n <= m holds
seq . m = r implies ( seq is convergent & lim seq = r ) )
assume A1: ex n being Nat st
for m being Nat st n <= m holds
seq . m = r ; :: thesis: ( seq is convergent & lim seq = r )
A2: for r1 being Real st 0 < r1 holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r).| < r1

proof

consider n being Nat such that
A3: for m being Nat st n <= m holds
seq . m = r by A1;
let r1 be Real; :: thesis: ( 0 < r1 implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r).| < r1 )
assume A4: 0 < r1 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r).| < r1
take n ; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - r).| < r1
let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - r).| < r1 )
assume n <= m ; :: thesis: |.((seq . m) - r).| < r1
then seq . m = r by A3;
hence |.((seq . m) - r).| < r1 by A4, ABSVALUE:2; :: 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