theorem Th56: :: AFINSQ_2:57

for rF1, rF2 being real-valued XFinSequence st len rF1 = len rF2 & ( for i being Nat st i in dom rF1 holds
rF1 . i <= rF2 . i ) holds
Sum rF1 <= Sum rF2