for f, g being FinSequence of REAL 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