let X be RealBanachSpace; :: thesis: for M being non empty Subset of X st M is linearly-closed & M is closed holds

NLin M is RealBanachSpace

let M be non empty Subset of X; :: thesis: ( M is linearly-closed & M is closed implies NLin M is RealBanachSpace )

assume A1: ( M is linearly-closed & M is closed ) ; :: thesis: NLin M is RealBanachSpace

then the carrier of (NLin M) = M by LCL1;

hence NLin M is RealBanachSpace by A1, LM76A; :: thesis: verum

NLin M is RealBanachSpace

let M be non empty Subset of X; :: thesis: ( M is linearly-closed & M is closed implies NLin M is RealBanachSpace )

assume A1: ( M is linearly-closed & M is closed ) ; :: thesis: NLin M is RealBanachSpace

then the carrier of (NLin M) = M by LCL1;

hence NLin M is RealBanachSpace by A1, LM76A; :: thesis: verum