:: deftheorem defines NLin NORMSP_3:def 5 :
for V being RealNormSpace
for V1 being Subset of V holds NLin V1 = NORMSTR(# the carrier of (Lin V1),(0. (Lin V1)), the addF of (Lin V1), the Mult of (Lin V1),(Norm_ ( the carrier of (Lin V1),V)) #);