theorem :: DBLSEQ_1:7

for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is P-convergent iff Rseq is Cauchy )