dom (v tohilbval) = NAT by Lm15;
hence v tohilbval is total by PARTFUN1:def 2; :: thesis: verum