let i, j be Instruction of SCM+FSA; :: thesis: card (i ";" j) = 4
thus card (i ";" j) = (card (Macro i)) + (card (Macro j)) by Th11
.= (card (Macro i)) + 2 by COMPOS_1:56
.= 2 + 2 by COMPOS_1:56
.= 4 ; :: thesis: verum