let t be Element of NAT ; :: thesis: 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)))}
let f be Function of [:NAT,NAT:],R^1; :: thesis: 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)))}
let seq be Function of [:NAT,NAT:],REAL; :: thesis: ( f = seq & ( for x being Element of NAT holds lim_filter ((ProjMap1 (f,x)),(Frechet_Filter NAT)) <> {} ) implies lim_filter ((ProjMap1 (f,t)),(Frechet_Filter NAT)) = {(lim (ProjMap1 (seq,t)))} )
assume that
A1: f = seq and
A2: for x being Element of NAT holds lim_filter ((ProjMap1 (f,x)),(Frechet_Filter NAT)) <> {} ; :: thesis: lim_filter ((ProjMap1 (f,t)),(Frechet_Filter NAT)) = {(lim (ProjMap1 (seq,t)))}
( not lim_filter ((ProjMap1 (f,t)),(Frechet_Filter NAT)) is empty & lim_filter ((ProjMap1 (f,t)),(Frechet_Filter NAT)) is trivial ) by A2;
then consider x being object such that
A3: lim_filter ((ProjMap1 (f,t)),(Frechet_Filter NAT)) = {x} by ZFMISC_1:131;
reconsider f1 = ProjMap1 (f,t) as Function of NAT,R^1 ;
reconsider seq1 = ProjMap1 (seq,t) as Function of NAT,REAL ;
lim_f f1 = {(lim seq1)} by A1, A3, Th72;
hence lim_filter ((ProjMap1 (f,t)),(Frechet_Filter NAT)) = {(lim (ProjMap1 (seq,t)))} ; :: thesis: verum