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 ; :: thesis: verum
end;
then seq is convergent by SEQ_2:def 6;
hence ( seq is convergent & lim seq = r ) by ; :: thesis: verum