theorem Th8: :: REAL_NS3:8

for n being non empty Nat
for x being Element of REAL n ex xMAX being Real st
( xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) )