theorem Th94: :: DBLSEQ_3:94

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 )