for seq being nonnegative ExtREAL_sequence st not Partial_Sums seq is convergent_to_+infty holds
for n being Nat holds seq . n is Real