theorem Th3: :: INTEGRA5:3

for F1, F2 being FinSequence of REAL st len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds
F1 . i <= F2 . i ) holds
Sum F1 <= Sum F2