:: deftheorem defines ||. NORMSP_0:def 4 :
for X being non empty N-Str
for s being sequence of X
for b₃ being Real_Sequence holds
( b₃ = ||.s.|| iff for n being Nat holds b₃ . n = ||.(s . n).|| );