let t be Element of NAT ; :: thesis: for f being Function of ,R^1
for seq being Function of ,REAL st f = seq & ( for x being Element of NAT holds lim_filter ((ProjMap2 (f,x)),) <> {} ) holds
lim_filter ((ProjMap2 (f,t)),) = {(lim (ProjMap2 (seq,t)))}

let f be Function of ,R^1; :: thesis: for seq being Function of ,REAL st f = seq & ( for x being Element of NAT holds lim_filter ((ProjMap2 (f,x)),) <> {} ) holds
lim_filter ((ProjMap2 (f,t)),) = {(lim (ProjMap2 (seq,t)))}

let seq be Function of ,REAL; :: thesis: ( f = seq & ( for x being Element of NAT holds lim_filter ((ProjMap2 (f,x)),) <> {} ) implies lim_filter ((ProjMap2 (f,t)),) = {(lim (ProjMap2 (seq,t)))} )
assume that
A1: f = seq and
A2: for x being Element of NAT holds lim_filter ((ProjMap2 (f,x)),) <> {} ; :: thesis: lim_filter ((ProjMap2 (f,t)),) = {(lim (ProjMap2 (seq,t)))}
( not lim_filter ((ProjMap2 (f,t)),) is empty & lim_filter ((ProjMap2 (f,t)),) is trivial ) by A2;
then consider x being object such that
A3: lim_filter ((ProjMap2 (f,t)),) = {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)),) = {(lim (ProjMap2 (seq,t)))} ; :: thesis: verum