theorem Th34: :: REAL_NS3:33

for S, T being RealNormSpace
for I being LinearOperator of S,T
for s1 being sequence of S st I is one-to-one & I is onto & I is isometric-like & s1 is convergent holds
( I * s1 is convergent & lim (I * s1) = I . (lim s1) )