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