for V being RealNormSpace
for W being SubRealNormSpace of V st the carrier of W = the carrier of V holds
NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #) = NORMSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the normF of V #)