theorem :: SERIES_3:40

for n being Nat
for s, s1, s2 being Real_Sequence st s = s1 (#) s2 & ( for n being Nat holds
( s1 . n < 0 & s2 . n < 0 ) ) holds
(Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)