theorem LM021: :: NDIFF_7:10

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