deffunc H₁( Element of NAT ) -> set = F . $1,n;
consider IT being Function such that
A1: ( dom IT = NAT & ( for m being Element of NAT holds IT . m = H₁(m) ) ) from FUNCT_1:sch 4();

now

let y be set ; :: thesis: ( y in rng IT implies y in PFuncs X,Y )
assume y in rng IT ; :: thesis: y in PFuncs X,Y
then consider k being set such that
A2: ( k in dom IT & y = IT . k ) by FUNCT_1:def 5;
reconsider k = k as Element of NAT by A1, A2;
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
y = F . k,n1 by A1, A2;
hence y in PFuncs X,Y ; :: thesis: verum

end;

then rng IT c= PFuncs X,Y by TARSKI:def 3;
then reconsider IT = IT as Functional_Sequence of X,Y by A1, FUNCT_2:def 1, RELSET_1:11;
take IT ; :: thesis: for m being Nat holds IT . m = F . m,n
thus for m being Nat holds IT . m = F . m,n :: thesis: verum

proof

let m be Nat; :: thesis: IT . m = F . m,n
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 13;
IT . m = F . m1,n1 by A1;
hence IT . m = F . m,n ; :: thesis: verum

end;