:: deftheorem defines ||. NORMSP_0:def 1 :
for X being non empty N-Str
for x being Element of X holds ||.x.|| = the normF of X . x;