let S1 be sequence of RealSpace; :: thesis: for seq being Real_Sequence
for g being Real
for g1 being Element of RealSpace st S1 = seq & g = g1 holds
( seq is convergent & lim seq = g iff ( S1 is convergent & lim S1 = g1 ) )
let seq be Real_Sequence; :: thesis: for g being Real
for g1 being Element of RealSpace st S1 = seq & g = g1 holds
( seq is convergent & lim seq = g iff ( S1 is convergent & lim S1 = g1 ) )
let g be Real; :: thesis: for g1 being Element of RealSpace st S1 = seq & g = g1 holds
( seq is convergent & lim seq = g iff ( S1 is convergent & lim S1 = g1 ) )
let g1 be Element of RealSpace; :: thesis: ( S1 = seq & g = g1 implies ( seq is convergent & lim seq = g iff ( S1 is convergent & lim S1 = g1 ) ) )
assume AS: ( S1 = seq & g = g1 ) ; :: thesis: ( seq is convergent & lim seq = g iff ( S1 is convergent & lim S1 = g1 ) )

hereby :: thesis: ( S1 is convergent & lim S1 = g1 implies ( seq is convergent & lim seq = g ) )

assume ( seq is convergent & lim seq = g ) ; :: thesis: ( S1 is convergent & lim S1 = g1 )
then for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p by SEQ_2:def 7;
then A1: 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 AS, Th23;
hence S1 is convergent ; :: thesis: lim S1 = g1
hence lim S1 = g1 by A1, TBSP_1:def 3; :: thesis: verum

end;

assume ( S1 is convergent & lim S1 = g1 ) ; :: thesis: ( seq is convergent & lim seq = g )
then 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 TBSP_1:def 3;
then A2: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p by AS, Th23;
hence seq is convergent by SEQ_2:def 6; :: thesis: lim seq = g
hence lim seq = g by A2, SEQ_2:def 7; :: thesis: verum