let i be Instruction of SCM+FSA; (Directed (Macro i)) . 1 = goto 2
A1:
(Macro i) . 1 = halt SCM+FSA
by COMPOS_1:59;
1 in {0,1}
by TARSKI:def 2;
then A2:
1 in dom (Macro i)
by COMPOS_1:61;
A3:
halt SCM+FSA in dom ((halt SCM+FSA) .--> (goto 2))
by TARSKI:def 1;
A4:
dom (id the InstructionsF of SCM+FSA) = the InstructionsF of SCM+FSA
;
( card (Macro i) = 2 & rng (Macro i) c= the InstructionsF of SCM+FSA )
by COMPOS_1:56, RELAT_1:def 19;
hence (Directed (Macro i)) . 1 =
(((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto 2))) * (Macro i)) . 1
by FUNCT_7:116
.=
(((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) * (Macro i)) . 1
by A4, FUNCT_7:def 3
.=
((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) . (halt SCM+FSA)
by A2, A1, FUNCT_1:13
.=
((halt SCM+FSA) .--> (goto 2)) . (halt SCM+FSA)
by A3, FUNCT_4:13
.=
goto 2
by FUNCOP_1:72
;
verum