for G being RealNormSpace-Sequence
for x, y being Point of (product G)
for Z, x0 being Element of product (carr G)
for X being set st Z = 0. (product G) & x0 = x & y = Z +* (x0 | X) holds
||.y.|| <= ||.x.||