card (abs p) = card (dom p) by VALUED_1:def 11
.= n by CARD_1:def 7 ;
hence abs p is n -element by CARD_1:def 7; :: thesis: verum