let V be RealNormSpace; :: thesis: for W being Subspace of V holds RSubNormSpace W is SubRealNormSpace of V
let W be Subspace of V; :: thesis: RSubNormSpace W is SubRealNormSpace of V
set X = RSubNormSpace W;
( RLSStruct(# the carrier of (RSubNormSpace W), the ZeroF of (RSubNormSpace W), the addF of (RSubNormSpace W), the Mult of (RSubNormSpace W) #) = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) & the normF of (RSubNormSpace W) = the normF of V | the carrier of (RSubNormSpace W) ) by Def1;
then ( the carrier of (RSubNormSpace W) = the carrier of W & 0. (RSubNormSpace W) = 0. W & the addF of (RSubNormSpace W) = the addF of W & the Mult of (RSubNormSpace W) = the Mult of W ) ;
then ( the carrier of (RSubNormSpace W) c= the carrier of V & 0. (RSubNormSpace W) = 0. V & the addF of (RSubNormSpace W) = the addF of V || the carrier of (RSubNormSpace W) & the Mult of (RSubNormSpace W) = the Mult of V | [:REAL, the carrier of (RSubNormSpace W):] & the normF of (RSubNormSpace W) = the normF of V | the carrier of (RSubNormSpace W) ) by RLSUB_1:def 2, Def1;
hence RSubNormSpace W is SubRealNormSpace of V by DUALSP01:def 16; :: thesis: verum