for s, t being Real_Sequence
for g being Real st ( for n being Element of NAT holds t . n = |.((s . n) - g).| ) holds
( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) )