for f, g being summable Real_Sequence st ( for n being Nat holds f . n <= g . n ) holds
Sum f <= Sum g