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