take NAT --> the NAT * -defined to-naturals homogeneous Function ; :: thesis: NAT --> the NAT * -defined to-naturals homogeneous Function is satisfying_primrec_conditions
thus NAT --> the NAT * -defined to-naturals homogeneous Function is satisfying_primrec_conditions ; :: thesis: verum