:: deftheorem Def2 defines ||. NORMSP_0:def 2 :
for X being non empty N-Str
for f being the carrier of b₁ -valued Function
for b₃ being Function holds
( b₃ = ||.f.|| iff ( dom b₃ = dom f & ( for e being set st e in dom b₃ holds
b₃ . e = ||.(f /. e).|| ) ) );