for seq being ExtREAL_sequence st ( for n being Nat holds 0 < seq . n ) holds
for m being Nat holds 0 < (Partial_Sums seq) . m