:: deftheorem defines ||. NORMSP_0:def 3 :
for C being non empty set
for X being non empty N-Str
for f being PartFunc of C, the carrier of X
for b₄ being PartFunc of C,REAL holds
( b₄ = ||.f.|| iff ( dom b₄ = dom f & ( for c being Element of C st c in dom b₄ holds
b₄ . c = ||.(f /. c).|| ) ) );