dom (f - c) = dom ((- c) + f) by VALUED_1:def 3
.= dom f by VALUED_1:def 2 ;
hence f - c is total by PARTFUN1:def 2; :: thesis: verum