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