for Rseq being Function of [:NAT,NAT:],REAL
for r being Real st Rseq is P-convergent holds
( r (#) Rseq is P-convergent & P-lim (r (#) Rseq) = r * (P-lim Rseq) )