deffunc H₁( Element of NAT * ) -> Element of omega = ($1 . i) + 1;
defpred S₁[ set ] means $1 in n -tuples_on NAT;
consider f being PartFunc of (NAT *),NAT such that
A1: for d being Element of NAT * holds
( d in dom f iff S₁[d] ) and
A2: for d being Element of NAT * st d in dom f holds
f /. d = H₁(d) from PARTFUN2:sch 2();
A3: n -tuples_on NAT c= NAT * by FINSEQ_2:142;
then A4: for x being object holds
( x in dom f iff x in n -tuples_on NAT ) by A1;
then A5: dom f = n -tuples_on NAT by TARSKI:2;
reconsider f = f as Element of PFuncs ((NAT *),NAT) by PARTFUN1:45;
f is homogeneous by A5;
then f in { g where g is Element of PFuncs ((NAT *),NAT) : g is homogeneous } ;
then reconsider f = f as Element of HFuncs NAT ;
take f ; :: thesis: ( dom f = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds f . p = (p . i) + 1 ) )
thus dom f = n -tuples_on NAT by A4; :: thesis: for p being Element of n -tuples_on NAT holds f . p = (p . i) + 1
let p be Element of n -tuples_on NAT; :: thesis: f . p = (p . i) + 1
reconsider p9 = p as Element of NAT * by A3;
thus f . p = f /. p9 by A5, PARTFUN1:def 6
.= (p . i) + 1 by A2, A5 ; :: thesis: verum