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