A1: dom (proj ((n |-> NAT),i)) = product (n |-> NAT) by CARD_3:def 16
.= n -tuples_on NAT by FINSEQ_3:131 ;

now :: thesis: proj ((n |-> NAT),i) is Element of HFuncs NAT

set P = proj ((n |-> NAT),i);
A2: rng (proj ((n |-> NAT),i)) c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (proj ((n |-> NAT),i)) or x in NAT )
assume x in rng (proj ((n |-> NAT),i)) ; :: thesis: x in NAT
then consider d being object such that
A3: d in dom (proj ((n |-> NAT),i)) and
A4: x = (proj ((n |-> NAT),i)) . d by FUNCT_1:def 3;
reconsider d = d as Element of n -tuples_on NAT by A1, A3;
reconsider d = d as FinSequence of NAT ;
(proj ((n |-> NAT),i)) . d = d . i by A3, CARD_3:def 16;
hence x in NAT by A4; :: thesis: verum

end;

A5: proj ((n |-> NAT),i) is homogeneous

proof

thus dom (proj ((n |-> NAT),i)) is with_common_domain ; :: according to MARGREL1:def 21 :: thesis: verum

end;

reconsider P = proj ((n |-> NAT),i) as PartFunc of (NAT *),NAT by A1, A2, FINSEQ_2:142, RELSET_1:4;
P is Element of PFuncs ((NAT *),NAT) by PARTFUN1:45;
then P in HFuncs NAT by A5;
hence proj ((n |-> NAT),i) is Element of HFuncs NAT ; :: thesis: verum

end;

hence proj ((n |-> NAT),i) is NAT * -defined to-naturals homogeneous Function ; :: thesis: verum