for f, g being Real_Sequence
for N being Element of NAT
for c being Real st f is convergent & lim f = c & ( for n being Element of NAT st n >= N holds
f . n = g . n ) holds
( g is convergent & lim g = c ) by Lm22;