for f being NAT * -defined to-naturals homogeneous len-total Function holds f is quasi_total Element of HFuncs NAT