let seq be ExtREAL_sequence; :: thesis: for r being real number st ( for n being Nat holds seq . n = r ) holds
( seq is convergent_to_finite_number & lim seq = r )
let r be real number ; :: 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

reconsider n = 1 as Nat ;
let p be real number ; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (R_EAL r)).| < p )
assume A3: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (R_EAL r)).| < p
take n = n; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - (R_EAL r)).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - (R_EAL r)).| < p )
assume n <= m ; :: thesis: |.((seq . m) - (R_EAL r)).| < p
seq . m = R_EAL r by A1;
then (seq . m) - (R_EAL r) = 0 by XXREAL_3:7;
hence |.((seq . m) - (R_EAL r)).| < p by A3, EXTREAL2:5; :: thesis: verum

end;

hence A4: seq is convergent_to_finite_number by Def8; :: thesis: lim seq = r
then seq is convergent by Def11;
hence lim seq = r by A2, A4, Def12; :: thesis: verum