let A be finite set ; :: thesis: len (canFS A) = card A
thus card (canFS A) = card (dom (canFS A)) by CARD_1:62
.= card (rng (canFS A)) by CARD_1:70
.= card A by FUNCT_2:def 3 ; :: thesis: verum