deffunc H₁( Element of NAT * ) -> Element of NAT = ($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 set holds
( x in dom f iff x in n -tuples_on NAT ) by A1;
then A5: dom f = n -tuples_on NAT by TARSKI:1;
reconsider f = f as Element of PFuncs ((NAT *),NAT) by PARTFUN1:45;
f is homogeneous

proof

thus dom f is with_common_domain by A5; :: according to MARGREL1:def 21 :: thesis: verum

end;

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, TARSKI:1; :: 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
p in n -tuples_on NAT ;
then 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