:: deftheorem DefSubSP defines SubRealNormSpace DUALSP01:def 16 :
for V, b₂ being RealNormSpace holds
( b₂ is SubRealNormSpace of V iff ( the carrier of b₂ c= the carrier of V & 0. b₂ = 0. V & the addF of b₂ = the addF of V || the carrier of b₂ & the Mult of b₂ = the Mult of V | [:REAL, the carrier of b₂:] & the normF of b₂ = the normF of V | the carrier of b₂ ) );