defpred S1[ Element of NAT , set ] means $2 = lim (ProjMap2 (Rseq,$1));
a1: now :: thesis: for m being Element of NAT ex n being Element of REAL st S1[m,n]
let m be Element of NAT ; :: thesis: ex n being Element of REAL st S1[m,n]
reconsider n = lim (ProjMap2 (Rseq,m)) as Element of REAL by XREAL_0:def 1;
take n = n; :: thesis: S1[m,n]
thus S1[m,n] ; :: thesis: verum
end;
consider IT being Function of NAT,REAL such that
a2: for m being Element of NAT holds S1[m,IT . m] from FUNCT_2:sch 3(a1);
 take IT ; :: thesis: for m being Element of NAT holds IT . m = lim (ProjMap2 (Rseq,m))
thus for m being Element of NAT holds IT . m = lim (ProjMap2 (Rseq,m)) by a2; :: thesis: verum