dom (proj (f,x)) = {{}} by CARD_3:10, CARD_3:def 16;
hence proj (f,x) is trivial ; :: thesis: verum