theorem Th11: :: PRVECT_2:11

for G being RealNormSpace-Sequence
for i being Element of dom G
for x, y being Point of (product G)
for xi, yi being Point of (G . i)
for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds
||.(yi - xi).|| <= ||.(y - x).||