theorem Th5: :: MATRPROB:5

for e being real-valued FinSequence 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