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