for s1, s2 being Real_Sequence st ( for n being Nat holds s1 . n <= s2 . n ) holds
for n being Nat holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n