let S, T be RealNormSpace; :: thesis: for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric-like & Z is closed holds
I .: Z is closed
let I be LinearOperator of S,T; :: thesis: for Z being Subset of S st I is one-to-one & I is onto & I is isometric-like & Z is closed holds
I .: Z is closed
let Z be Subset of S; :: thesis: ( I is one-to-one & I is onto & I is isometric-like & Z is closed implies I .: Z is closed )
assume that
A1: ( I is one-to-one & I is onto ) and
A2: I is isometric-like and
A3: Z is closed ; :: thesis: I .: Z is closed
A4: dom I = the carrier of S by FUNCT_2:def 1;
consider J being LinearOperator of T,S such that
A5: ( J = I " & J is one-to-one & J is onto & J is isometric-like ) by A1, A2, Th29;
A6: rng I = the carrier of T by A1, FUNCT_2:def 3;

now :: thesis: for t1 being sequence of T st rng t1 c= I .: Z & t1 is convergent holds
lim t1 in I .: Z

let t1 be sequence of T; :: thesis: ( rng t1 c= I .: Z & t1 is convergent implies lim t1 in I .: Z )
assume A7: ( rng t1 c= I .: Z & t1 is convergent ) ; :: thesis: lim t1 in I .: Z
then A8: J * t1 is convergent by A5, Th35;
A9: rng (J * t1) = J .: (rng t1) by RELAT_1:127;
J .: (I .: Z) = I " (I .: Z) by A1, A5, FUNCT_1:85
.= Z by A1, A4, FUNCT_1:94 ;
then lim (J * t1) in Z by A3, A7, A8, A9, RELAT_1:123;
then J . (lim t1) in Z by A5, A7, Th34;
then I . (J . (lim t1)) in I .: Z by FUNCT_2:35;
hence lim t1 in I .: Z by A1, A5, A6, FUNCT_1:35; :: thesis: verum

end;

hence I .: Z is closed ; :: thesis: verum