:: deftheorem DefNorm defines Norm_ NORMSP_3:def 4 :
for X being RealNormSpace
for X1 being set st X1 c= the carrier of X holds
Norm_ (X1,X) = the normF of X | X1;