let I be preProgram of SCM+FSA; :: thesis: for l being Element of NAT holds card (Directed (I,l)) = card I
let l be Element of NAT ; :: thesis: card (Directed (I,l)) = card I
thus card (Directed (I,l)) = card (dom (Directed (I,l))) by CARD_1:62
.= card (dom I) by FUNCT_4:99
.= card I by CARD_1:62 ; :: thesis: verum