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