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