theorem Th41: :: SERIES_3:41
for s being Real_Sequence
for n being Nat holds |.((Partial_Sums s) . n).| <= (Partial_Sums (abs s)) . n