theorem :: NEWTON04:31

for f being real-valued FinSequence
for g being real-valued nonnegative-yielding FinSequence st ( for x being Nat holds f . x >= g . x ) holds
f is nonnegative-yielding