consider c being Cardinal such that
A1: dom f = c ;
c = card (dom f) by A1;
hence dom f = card f by CARD_1:62; :: thesis: verum