let i be Instruction of SCM+FSA ; :: thesis: ( ( i = halt SCM+FSA implies (Directed (Macro i)) . (insloc 0 ) = goto (insloc 2) ) & ( i <> halt SCM+FSA implies (Directed (Macro i)) . (insloc 0 ) = i ) )
insloc 0 in {(insloc 0 ),(insloc 1)} by TARSKI:def 2;
then A1: insloc 0 in dom (Macro i) by Th4;
A2: card (Macro i) = 2 by Th6;
A3: (Macro i) . (insloc 0 ) = i by SCMFSA6B:33;

hereby :: thesis: ( i <> halt SCM+FSA implies (Directed (Macro i)) . (insloc 0 ) = i )

assume A4: i = halt SCM+FSA ; :: thesis: (Directed (Macro i)) . (insloc 0 ) = goto (insloc 2)
dom ((halt SCM+FSA ) .--> (goto (insloc 2))) = {(halt SCM+FSA )} by FUNCOP_1:19;
then A5: i in dom ((halt SCM+FSA ) .--> (goto (insloc 2))) by A4, TARSKI:def 1;
dom (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
then X: halt SCM+FSA in dom (id the Instructions of SCM+FSA ) ;
rng (Macro i) c= the Instructions of SCM+FSA by AMI_1:118;
hence (Directed (Macro i)) . (insloc 0 ) = (((id the Instructions of SCM+FSA ) +* (halt SCM+FSA ),(goto (insloc 2))) * (Macro i)) . (insloc 0 ) by A2, FUNCT_7:118
.= (((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc 2)))) * (Macro i)) . (insloc 0 ) by X, FUNCT_7:def 3
.= ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc 2)))) . i by A1, A3, FUNCT_1:23
.= ((halt SCM+FSA ) .--> (goto (insloc 2))) . i by A5, FUNCT_4:14
.= goto (insloc 2) by A4, FUNCOP_1:87 ;
:: thesis: verum

end;

assume A6: i <> halt SCM+FSA ; :: thesis: (Directed (Macro i)) . (insloc 0 ) = i
dom ((halt SCM+FSA ) .--> (goto (insloc 2))) = {(halt SCM+FSA )} by FUNCOP_1:19;
then A7: not i in dom ((halt SCM+FSA ) .--> (goto (insloc 2))) by A6, TARSKI:def 1;
dom (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
then X: halt SCM+FSA in dom (id the Instructions of SCM+FSA ) ;
rng (Macro i) c= the Instructions of SCM+FSA by AMI_1:118;
hence (Directed (Macro i)) . (insloc 0 ) = (((id the Instructions of SCM+FSA ) +* (halt SCM+FSA ),(goto (insloc 2))) * (Macro i)) . (insloc 0 ) by A2, FUNCT_7:118
.= (((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc 2)))) * (Macro i)) . (insloc 0 ) by X, FUNCT_7:def 3
.= ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc 2)))) . i by A1, A3, FUNCT_1:23
.= (id the Instructions of SCM+FSA ) . i by A7, FUNCT_4:12
.= i by FUNCT_1:35 ;
:: thesis: verum