:: deftheorem Def12 defines productnorm PRVECT_2:def 12 :
for G being RealNormSpace-Sequence
for b₂ being Function of (product (carr G)),REAL holds
( b₂ = productnorm G iff for x being Element of product (carr G) holds b₂ . x = |.(normsequence (G,x)).| );