theorem :: CARDFIL4:92

for Rseq being Function of [:NAT,NAT:],REAL
for Y being non empty Hausdorff TopSpace
for f being Function of [:NAT,NAT:],Y st ( for x being Element of NAT holds lim_filter ((ProjMap2 (f,x)),(Frechet_Filter NAT)) <> {} ) & f = Rseq & Y = R^1 holds
lim_in_cod1 (f,(Frechet_Filter NAT)) = lim_in_cod1 Rseq