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

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

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

then
seq is convergent
by SEQ_2:def 6;
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;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

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