let I be preProgram of SCM+FSA ; :: thesis: for l being Instruction-Location of SCM+FSA holds card (Directed I,l) = card I
let l be Instruction-Location of SCM+FSA ; :: 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