let f be Element of HFuncs NAT; :: thesis: ( f is primitive-recursive implies f is quasi_total )
assume f in PrimRec ; :: according to COMPUT_1:def 16 :: thesis: f is quasi_total
hence f is quasi_total ; :: thesis: verum