theorem :: DBLSEQ_3:95

for f being Function of [:NAT,NAT:],ExtREAL
for r being Real st ( for n, m being Nat holds f . (n,m) = r ) holds
( f is P-convergent_to_finite_number & P-lim f = r )