let seq be ExtREAL_sequence; :: thesis: for r being Real st ( for n being Nat holds seq . n = r ) holds

( seq is convergent_to_finite_number & lim seq = r )

let r be Real; :: thesis: ( ( for n being Nat holds seq . n = r ) implies ( seq is convergent_to_finite_number & lim seq = r ) )

assume A1: for n being Nat holds seq . n = r ; :: thesis: ( seq is convergent_to_finite_number & lim seq = r )

then A5: seq is convergent ;

reconsider r = r as R_eal by XXREAL_0:def 1;

ex g being Real st

( r = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - r).| < p ) & seq is convergent_to_finite_number ) by A2, A4;

hence lim seq = r by Def12, A5; :: thesis: verum

( seq is convergent_to_finite_number & lim seq = r )

let r be Real; :: thesis: ( ( for n being Nat holds seq . n = r ) implies ( seq is convergent_to_finite_number & lim seq = r ) )

assume A1: for n being Nat holds seq . n = r ; :: thesis: ( seq is convergent_to_finite_number & lim seq = r )

A2: now :: thesis: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - r).| < p

hence A4:
seq is convergent_to_finite_number
; :: thesis: lim seq = rex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - r).| < p

reconsider n = 1 as Nat ;

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - r).| < p )

assume A3: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - r).| < p

take n = n; :: thesis: for m being Nat st n <= m holds

|.((seq . m) - r).| < p

let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - r).| < p )

assume n <= m ; :: thesis: |.((seq . m) - r).| < p

seq . m = r by A1;

then (seq . m) - r = 0 by XXREAL_3:7;

then |.((seq . m) - r).| = 0 by EXTREAL1:16;

hence |.((seq . m) - r).| < p by A3; :: thesis: verum

end;let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - r).| < p )

assume A3: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - r).| < p

take n = n; :: thesis: for m being Nat st n <= m holds

|.((seq . m) - r).| < p

let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - r).| < p )

assume n <= m ; :: thesis: |.((seq . m) - r).| < p

seq . m = r by A1;

then (seq . m) - r = 0 by XXREAL_3:7;

then |.((seq . m) - r).| = 0 by EXTREAL1:16;

hence |.((seq . m) - r).| < p by A3; :: thesis: verum

then A5: seq is convergent ;

reconsider r = r as R_eal by XXREAL_0:def 1;

ex g being Real st

( r = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - r).| < p ) & seq is convergent_to_finite_number ) by A2, A4;

hence lim seq = r by Def12, A5; :: thesis: verum