A1: dom (proj (n |-> NAT ),i) = product (n |-> NAT ) by CARD_3:def 17
.= n -tuples_on NAT by FUNCT_6:9 ;

now

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

proof

let x be set ; :: 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 set such that
A3: d in dom (proj (n |-> NAT ),i) and
A4: x = (proj (n |-> NAT ),i) . d by FUNCT_1:def 5;
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 17;
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 by A1; :: according to MARGREL1:def 22 :: thesis: verum

end;

reconsider P = proj (n |-> NAT ),i as PartFunc of (NAT * ),NAT by A1, A2, FINSEQ_2:162, RELSET_1:11;
P is Element of PFuncs (NAT * ),NAT by PARTFUN1:119;
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