theorem NYS: :: NEWTON04:32

for f, g being real-valued FinSequence st ( for x being Nat holds f . x >= g . x ) holds
Sum f >= Sum g