for f, g being FinSequence of REAL st ( for x being Nat holds f . x >= g . x ) holds
Sum f >= Sum g