let i be Instruction of SCM+FSA ; :: thesis: (Directed (Macro i)) . 1 = goto 2
A1: (Macro i) . 1 = halt SCM+FSA by SCMFSA6B:33;
1 in {0 ,1} by TARSKI:def 2;
then A2: 1 in dom (Macro i) by Th4;
dom ((halt SCM+FSA ) .--> (goto 2)) = {(halt SCM+FSA )} by FUNCOP_1:19;
then A3: halt SCM+FSA in dom ((halt SCM+FSA ) .--> (goto 2)) by TARSKI:def 1;
A4: dom (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
( card (Macro i) = 2 & rng (Macro i) c= the Instructions of SCM+FSA ) by Th6, RELAT_1:def 19;
hence (Directed (Macro i)) . 1 = (((id the Instructions of SCM+FSA ) +* (halt SCM+FSA ),(goto 2)) * (Macro i)) . 1 by FUNCT_7:118
.= (((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto 2))) * (Macro i)) . 1 by A4, FUNCT_7:def 3
.= ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto 2))) . (halt SCM+FSA ) by A2, A1, FUNCT_1:23
.= ((halt SCM+FSA ) .--> (goto 2)) . (halt SCM+FSA ) by A3, FUNCT_4:14
.= goto 2 by FUNCOP_1:87 ;
:: thesis: verum