let V, E be set ; :: thesis: card V = card (V --> E)
thus card V = card [:V,{E}:] by CARD_1:69
.= card (V --> E) by FUNCOP_1:def 2 ; :: thesis: verum