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