theorem Th102: :: DBLSEQ_3:102

for f being Function of [:NAT,NAT:],ExtREAL
for c being ExtReal st ( for n, m being Nat holds f . (n,m) = c ) holds
( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )