let I be preProgram of SCM+FSA; :: thesis: card (Directed I) = card I
thus card (Directed I) = card (dom (Directed I)) by CARD_1:62
.= card (dom I) by FUNCT_4:99
.= card I by CARD_1:62 ; :: thesis: verum