theorem Th10: :: PRVECT_2:10

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