let V be RealNormSpace; :: thesis: for V1 being Subset of V holds NLin V1 is SubRealNormSpace of V
let V1 be Subset of V; :: thesis: NLin V1 is SubRealNormSpace of V
set l = NLin V1;
A1: the carrier of (NLin V1) c= the carrier of V by RLSUB_1:def 2;
A2: ( NLin V1 is reflexive & NLin V1 is discerning & NLin V1 is RealNormSpace-like & NLin V1 is vector-distributive & NLin V1 is scalar-distributive & NLin V1 is scalar-associative & NLin V1 is scalar-unital & NLin V1 is Abelian & NLin V1 is add-associative & NLin V1 is right_zeroed & NLin V1 is right_complementable ) by RSSPACE:15, XTh7;
A3: 0. (NLin V1) = 0. V by RLSUB_1:def 2;
A4: the addF of (NLin V1) = the addF of V || the carrier of (NLin V1) by RLSUB_1:def 2;
A5: the Mult of (NLin V1) = the Mult of V | [:REAL, the carrier of (NLin V1):] by RLSUB_1:def 2;
the normF of (NLin V1) = the normF of V | the carrier of (NLin V1) by A1, DefNorm;
hence NLin V1 is SubRealNormSpace of V by A1, A2, A3, A4, A5, DUALSP01:def 16; :: thesis: verum