theorem Th74: :: CARDFIL4:91

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 ((ProjMap2 (f,x)),(Frechet_Filter NAT)) <> {} ) holds
lim_filter ((ProjMap2 (f,t)),(Frechet_Filter NAT)) = {(lim (ProjMap2 (seq,t)))}