defpred S₁[ Element of NAT , set ] means $2 = lim (ProjMap1 (Rseq,$1));

a1: now :: thesis: for m being Element of NAT ex n being Element of REAL st S₁[m,n]

let m be Element of NAT ; :: thesis: ex n being Element of REAL st S₁[m,n]
reconsider n = lim (ProjMap1 (Rseq,m)) as Element of REAL by XREAL_0:def 1;
take n = n; :: thesis: S₁[m,n]
thus S₁[m,n] ; :: thesis: verum

end;

consider IT being Function of NAT,REAL such that
a2: for m being Element of NAT holds S₁[m,IT . m] from FUNCT_2:sch 3(a1);
take IT ; :: thesis: for n being Element of NAT holds IT . n = lim (ProjMap1 (Rseq,n))
thus for n being Element of NAT holds IT . n = lim (ProjMap1 (Rseq,n)) by a2; :: thesis: verum