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 compact holds
I .: Z is compact
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 compact holds
I .: Z is compact
let Z be Subset of S; :: thesis: ( I is one-to-one & I is onto & I is isometric-like & Z is compact implies I .: Z is compact )
assume A1: ( I is one-to-one & I is onto & I is isometric-like & Z is compact ) ; :: thesis: I .: Z is compact
dom I = the carrier of S by FUNCT_2:def 1;
hence I .: Z is compact by A1, Th33, NFCONT_1:32; :: thesis: verum