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 holds
( s1 is convergent iff I * s1 is convergent )
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 holds
( s1 is convergent iff I * s1 is convergent )
let s1 be sequence of S; :: thesis: ( I is one-to-one & I is onto & I is isometric-like implies ( s1 is convergent iff I * s1 is convergent ) )
assume A1: ( I is one-to-one & I is onto & I is isometric-like ) ; :: thesis: ( s1 is convergent iff I * s1 is convergent )
then consider J being LinearOperator of T,S such that
A2: ( J = I " & J is one-to-one & J is onto & J is isometric-like ) by Th29;
A3: rng I = the carrier of T by A1, FUNCT_2:def 3;
thus ( s1 is convergent implies I * s1 is convergent ) by Th34, A1; :: thesis: ( I * s1 is convergent implies s1 is convergent )
assume A4: I * s1 is convergent ; :: thesis: s1 is convergent
A5: rng s1 c= the carrier of S ;
J * (I * s1) = (J * I) * s1 by RELAT_1:36
.= (id the carrier of S) * s1 by A1, A2, A3, FUNCT_2:29
.= s1 by RELAT_1:53, A5 ;
hence s1 is convergent by A2, A4, Th34; :: thesis: verum