thus len p = card (dom p) by CARD_1:104
.= dom p by CARD_1:def 5 ; :: thesis: verum