defpred S₁[ Element of NAT , set ] means $2 = lim (ProjMap2 (f,$1));
A1: for m being Element of NAT ex n being Element of ExtREAL st S₁[m,n] ;
consider IT being Function of NAT,ExtREAL such that
A2: for m being Element of NAT holds S₁[m,IT . m] from FUNCT_2:sch 3(A1);
take IT ; :: thesis: for m being Element of NAT holds IT . m = lim (ProjMap2 (f,m))
thus for m being Element of NAT holds IT . m = lim (ProjMap2 (f,m)) by A2; :: thesis: verum