:: deftheorem Def11 defines normsequence PRVECT_2:def 11 :
for G being RealNormSpace-Sequence
for x being Element of product (carr G)
for b₃ being Element of REAL (len G) holds
( b₃ = normsequence (G,x) iff ( len b₃ = len G & ( for j being Element of dom G holds b₃ . j = the normF of (G . j) . (x . j) ) ) );