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

now

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

proof

let x, y be FinSequence; :: according to UNIALG_1:def 1 :: thesis: ( not x in dom (proj (n |-> NAT ),i) or not y in dom (proj (n |-> NAT ),i) or len x = len y )
assume A3: ( x in dom (proj (n |-> NAT ),i) & y in dom (proj (n |-> NAT ),i) ) ; :: thesis: len x = len y
thus len x = n by A1, A3, FINSEQ_2:109
.= len y by A1, A3, FINSEQ_2:109 ; :: thesis: verum

end;

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
A4: ( d in dom (proj (n |-> NAT ),i) & x = (proj (n |-> NAT ),i) . d ) by FUNCT_1:def 5;
reconsider d = d as Element of n -tuples_on NAT by A1, A4;
reconsider d = d as FinSequence of NAT ;
A5: (proj (n |-> NAT ),i) . d = d . i by A4, PRALG_3:def 2;
thus x in NAT by A4, A5; :: thesis: verum

end;

then reconsider P = proj (n |-> NAT ),i as PartFunc of NAT * , NAT by A1, MSUALG_1:12, RELSET_1:11;
P is Element of PFuncs (NAT * ),NAT by PARTFUN1:119;
then P in HFuncs NAT by A2;
hence proj (n |-> NAT ),i is Element of HFuncs NAT ; :: thesis: verum

end;

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