theorem Th93: :: DBLSEQ_3:93

for f being Function of [:NAT,NAT:],ExtREAL st f is P-convergent_to_+infty holds
( not f is P-convergent_to_-infty & not f is P-convergent_to_finite_number )