thus len p = card (dom p) by CARD_1:62
.= dom p ; :: thesis: verum