theorem Th8: :: REAL_NS1:8

for n being Nat
for x being Element of REAL n
for i being Nat st i in Seg n holds
|.(x . i).| <= |.x.|