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