for g being NAT * -defined to-naturals len-total Function holds g is quasi_total PartFunc of (NAT *),NAT