theorem Th14: :: SERIES_1:14
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