theorem Th7: :: REAL_NS1:7

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