theorem :: CARDFIL4:89

for Rseq being Function of [:NAT,NAT:],REAL holds
( ( for x being Element of NAT holds lim_filter ((ProjMap1 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ) iff Rseq is convergent_in_cod2 )