let S, T be RealNormSpace; :: thesis: for I being LinearOperator of S,T
for Z being Subset of S st I is isometric & 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 isometric & Z is compact holds
I .: Z is compact
let Z be Subset of S; :: thesis: ( I is isometric & Z is compact implies I .: Z is compact )
assume AS: ( I is isometric & 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 AS, LM015, NFCONT_1:32; :: thesis: verum