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

now :: thesis: for y being object st y in rng IT holds
y in PFuncs (X,Y)

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
let y be object ; :: 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 object such that
A7: k in dom IT and
A8: y = IT . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A6, A7;
y = F . (k,n1) by A6, A8;
hence y in PFuncs (X,Y) ; :: thesis: verum

end;

then rng IT c= PFuncs (X,Y) ;
then reconsider IT = IT as Functional_Sequence of X,Y by A6, FUNCT_2:def 1, RELSET_1:4;
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 12;
IT . m = F . (m1,n1) by A6;
hence IT . m = F . (m,n) ; :: thesis: verum

end;