for g being Element of HFuncs NAT
for f1, f2 being quasi_total Element of HFuncs NAT
for i being Element of NAT st g is_primitive-recursively_expressed_by f1,f2,i holds
( g is quasi_total & ( not f1 is empty implies not g is empty ) )