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:104
.= card (dom I) by FUNCT_4:105
.= card I by CARD_1:104 ; :: thesis: verum