dom f = dom (Carrier f) by PRALG_1:def 14;
hence not Carrier f is empty ; :: thesis: verum