let i be Instruction of SCM+FSA; :: thesis: for J being Program of SCM+FSA holds card (i ';' J) = (card J) + 2
let J be Program of SCM+FSA; :: thesis: card (i ';' J) = (card J) + 2
thus card (i ';' J) = (card (Macro i)) + (card J) by Th61
.= (card J) + 2 by COMPOS_1:150 ; :: thesis: verum