for s1, s2 being Real_Sequence
for n being Nat st s1,s2 are_fiberwise_equipotent & s1 is nonnegative holds
ex m being Nat st (Partial_Sums s1) . n <= (Partial_Sums s2) . m