let S, T be RealNormSpace; :: thesis: 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) )
let I be LinearOperator of S,T; :: thesis: 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) )
let s1 be sequence of S; :: thesis: ( I is one-to-one & I is onto & I is isometric-like & s1 is convergent implies ( I * s1 is convergent & lim (I * s1) = I . (lim s1) ) )
assume A1: ( I is one-to-one & I is onto & I is isometric-like & s1 is convergent ) ; :: thesis: ( I * s1 is convergent & lim (I * s1) = I . (lim s1) )
dom I = the carrier of S by FUNCT_2:def 1;
then A3: rng s1 c= dom I ;
I is_continuous_in lim s1 by A1, Th32;
then ( I /* s1 is convergent & I /. (lim s1) = lim (I /* s1) ) by A1, A3;
hence ( I * s1 is convergent & lim (I * s1) = I . (lim s1) ) by A3, FUNCT_2:def 11; :: thesis: verum