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