let S, T be RealNormSpace; :: thesis: 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) )
let I be LinearOperator of S,T; :: thesis: for s1 being sequence of S st I is isometric & s1 is convergent holds
( I * s1 is convergent & lim (I * s1) = I . (lim s1) )
let s1 be sequence of S; :: thesis: ( I is isometric & s1 is convergent implies ( I * s1 is convergent & lim (I * s1) = I . (lim s1) ) )
assume AS: ( I is isometric & s1 is convergent ) ; :: thesis: ( I * s1 is convergent & lim (I * s1) = I . (lim s1) )
P1: dom I = the carrier of S by FUNCT_2:def 1;
P22: rng s1 c= dom I by P1;
I is_continuous_in lim s1 by AS, LM010;
then ( I /* s1 is convergent & I /. (lim s1) = lim (I /* s1) ) by NFCONT_1:def 5, AS, P22;
hence ( I * s1 is convergent & lim (I * s1) = I . (lim s1) ) by P22, FUNCT_2:def 11; :: thesis: verum