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