defpred S₁[ Nat, object ] means $2 = ProjPMap1 ((F . $1),x);
A1: for n being Element of NAT ex f being Element of PFuncs (X2,Y) st S₁[n,f]

proof

let n be Element of NAT ; :: thesis: ex f being Element of PFuncs (X2,Y) st S₁[n,f]
reconsider f = ProjPMap1 ((F . n),x) as Element of PFuncs (X2,Y) by PARTFUN1:45;
take f ; :: thesis: S₁[n,f]
thus S₁[n,f] ; :: thesis: verum

end;

consider IT being Function of NAT,(PFuncs (X2,Y)) such that
A2: for n being Element of NAT holds S₁[n,IT . n] from FUNCT_2:sch 3(A1);
take IT ; :: thesis: for n being Nat holds IT . n = ProjPMap1 ((F . n),x)

hereby :: thesis: verum

let n be Nat; :: thesis: IT . n = ProjPMap1 ((F . n),x)
n is Element of NAT by ORDINAL1:def 12;
hence IT . n = ProjPMap1 ((F . n),x) by A2; :: thesis: verum

end;