for s1, s2 being Real_Sequence st ( for n being Nat holds
( s1 . n >= 0 & s2 . n >= 0 ) ) holds
for n being Nat holds ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n