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