:: deftheorem DefNrPro defines NrProduct LOPBAN10:def 9 :
for X being RealNormSpace-Sequence
for x being Point of (product X)
for b₃ being non negative Real holds
( b₃ = NrProduct x iff ex Nx being FinSequence of REAL st
( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & b₃ = Product Nx ) );