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

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