:: deftheorem defines P-convergent DBLSEQ_3:def 17 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is P-convergent iff ( f is P-convergent_to_finite_number or f is P-convergent_to_+infty or f is P-convergent_to_-infty ) );