for Pseq being P-convergent Function of [:NAT,NAT:],REAL
for Psubseq being subsequence of Pseq holds P-lim Psubseq = P-lim Pseq by LM114;