dom (c (#) f) = dom f by VALUED_1:def 5;
hence c (#) f is total by PARTFUN1:def 2; :: thesis: verum