A1: dom (proj ((n |-> NAT),i)) =
product (n |-> NAT)
by CARD_3:def 16
.=
n -tuples_on NAT
by FINSEQ_3:131
;
now proj ((n |-> NAT),i) is Element of HFuncs NATset P =
proj (
(n |-> NAT),
i);
A2:
rng (proj ((n |-> NAT),i)) c= NAT
A5:
proj (
(n |-> NAT),
i) is
homogeneous
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
;
verum end;
hence
proj ((n |-> NAT),i) is NAT * -defined to-naturals homogeneous Function
; verum