theorem NYS1: :: NEWTON04:39

for f, g being real-valued FinSequence st ( for x being Nat holds
( f . x >= g . x & ex i being Nat st f . (i + 1) > g . (i + 1) ) ) holds
Sum f > Sum g