theorem Th35: :: REAL_NS3:34

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 holds
( s1 is convergent iff I * s1 is convergent )