for G being RealNormSpace-Sequence
for x, y, z being Element of product (carr G)
for i being Nat st i in dom x & z = [:(addop G):] . (x,y) holds
(normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i