theorem :: SERIES_3:39

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