theorem Th31: :: NDIFF_5:31

for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Point of (product G) holds ||.((proj i) . x).|| <= ||.x.||