let i be Instruction of SCM+FSA ; :: thesis: card (Macro i) = 2
thus card (Macro i) = card (Load <*i,(halt SCM+FSA )*>) by Th5
.= len <*i,(halt SCM+FSA )*> by SCMFSA_7:25
.= 2 by FINSEQ_1:61 ; :: thesis: verum