for t being Element of NAT
for f being Function of [:NAT,NAT:],R^1
for seq being Function of [:NAT,NAT:],REAL st f = seq & ( for x being Element of NAT holds lim_filter ((ProjMap1 (f,x)),(Frechet_Filter NAT)) <> {} ) holds
lim_filter ((ProjMap1 (f,t)),(Frechet_Filter NAT)) = {(lim (ProjMap1 (seq,t)))}