for G being RealNormSpace-Sequence
for x being Element of product (carr G)
for i being Nat st i in dom x holds
0 <= (normsequence (G,x)) . i