theorem Th7: :: TOPMETR3:7

for a, b being Real
for S1 being sequence of (Closed-Interval-MSpace (a,b))
for S being sequence of RealSpace st S = S1 & a <= b holds
( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) )