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