:: deftheorem Def13 defines product PRVECT_2:def 13 :
for G being RealNormSpace-Sequence
for b₂ being non empty strict NORMSTR holds
( b₂ = product G iff ( RLSStruct(# the carrier of b₂, the ZeroF of b₂, the addF of b₂, the Mult of b₂ #) = product G & the normF of b₂ = productnorm G ) );