:: deftheorem Def1 defines RSubNormSpace DUALSP06:def 1 :
for V being RealNormSpace
for W being Subspace of V
for b₃ being strict RealNormSpace holds
( b₃ = RSubNormSpace W iff ( RLSStruct(# the carrier of b₃, the ZeroF of b₃, the addF of b₃, the Mult of b₃ #) = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) & the normF of b₃ = the normF of V | the carrier of b₃ ) );