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 holds
( Z is open iff I .: Z is open )
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 holds
( Z is open iff I .: Z is open )
let Z be Subset of S; :: thesis: ( I is one-to-one & I is onto & I is isometric-like implies ( Z is open iff I .: Z is open ) )
assume that
A1: ( I is one-to-one & I is onto ) and
A2: I is isometric-like ; :: thesis: ( Z is open iff I .: Z is open )
consider J being LinearOperator of T,S such that
A3: ( J = I " & J is one-to-one & J is onto & J is isometric-like ) by A1, A2, Th29;
A4: I = J " by A1, A3, FUNCT_1:43;
A5: J " Z = (J ") .: Z by A3, FUNCT_1:85
.= I .: Z by A1, A3, FUNCT_1:43 ;
I .: (Z `) = J " (Z `) by A4, A3, FUNCT_1:85
.= (I .: Z) ` by A5, FUNCT_2:100 ;
hence ( Z is open iff I .: Z is open ) by A1, A2, Th36; :: thesis: verum