defpred S₁[ Element of NAT , set ] means $2 = lim (ProjMap1 (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 n being Element of NAT holds IT . n = lim (ProjMap1 (f,n))
thus for n being Element of NAT holds IT . n = lim (ProjMap1 (f,n)) by A2; :: thesis: verum