theorem Th11: :: REAL_NS3:10

for n being Nat
for x being Element of REAL n
for xMAX being Real st xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) holds
( Sum (abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum (abs x) )