theorem Th5: :: MATRPROB:5

for e being FinSequence of REAL st ( for i being Nat st i in dom e holds
0 <= e . i ) holds
for k being Nat st k in dom e holds
e . k <= Sum e