dom |.f.| = dom f by VALUED_1:def 11;
hence not |.f.| is empty ; :: thesis: verum