theorem Th16: :: COMPUT_1:17

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