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 )
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
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;
hence A4: seq is convergent_to_finite_number ; :: thesis: 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