let S1 be sequence of RealSpace; :: thesis: for seq being Real_Sequence st S1 = seq & seq is convergent holds
( S1 is convergent & lim S1 = lim seq )
let seq be Real_Sequence; :: thesis: ( S1 = seq & seq is convergent implies ( S1 is convergent & lim S1 = lim seq ) )
assume A1: ( S1 = seq & seq is convergent ) ; :: thesis: ( S1 is convergent & lim S1 = lim seq )
reconsider g1 = lim seq as Point of RealSpace by XREAL_0:def 1;
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p by A1, SEQ_2:def 7;
then A2: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p by A1, Th23;
hence S1 is convergent ; :: thesis: lim S1 = lim seq
hence lim S1 = lim seq by A2, TBSP_1:def 3; :: thesis: verum