reconsider f = NAT --> (k succ k) as Function-yielding homogeneous ManySortedSet of NAT ;
take f ; :: thesis: ( f is k -ary & f is primitive-recursive & f is to-naturals & f is NAT * -defined )
thus f is k -ary by FUNCOP_1:7, ORDINAL1:def 12; :: thesis: ( f is primitive-recursive & f is to-naturals & f is NAT * -defined )
thus f is primitive-recursive ; :: thesis: ( f is to-naturals & f is NAT * -defined )
thus f is to-naturals ; :: thesis: f is NAT * -defined
thus f is NAT * -defined ; :: thesis: verum