deffunc H1( Element of NAT ) -> set = F . (n,$1);
consider IT being Function such that
A1: ( dom IT = NAT & ( for m being Element of NAT holds IT . m = H1(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
A2: k in dom IT and
A3: y = IT . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A1, A2;
y = F . (n1,k) by A1, A3;
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 A1, FUNCT_2:def 1, RELSET_1:4;
take IT ; :: thesis: for m being Nat holds IT . m = F . (n,m)
thus for m being Nat holds IT . m = F . (n,m) :: thesis: verum
proof
let m be Nat; :: thesis: IT . m = F . (n,m)
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
IT . m = F . (n1,m1) by A1;
hence IT . m = F . (n,m) ; :: thesis: verum
end;