dom f is trivial ;
then dom (Card f) is trivial by CARD_3:def 2;
hence Card f is trivial ; :: thesis: verum