for S1 being sequence of RealSpace
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 ) )