for V being RealNormSpace
for V1 being Subset of V holds NLin V1 is SubRealNormSpace of V