let f be NAT * -defined to-naturals homogeneous len-total Function; :: thesis: f is quasi_total Element of HFuncs NAT
reconsider f9 = f as Element of HFuncs NAT by Th27;
f9 is quasi_total by Def2;
hence f is quasi_total Element of HFuncs NAT ; :: thesis: verum