dom (c (#) F) = dom F by VALUED_1:def 5;
hence c (#) F is empty ; :: thesis: verum