A1: dom (id the InstructionsF of SCM+FSA) = the InstructionsF of SCM+FSA ;
let i be Instruction of SCM+FSA; :: thesis: ( ( i = halt SCM+FSA implies (Directed (Macro i)) . 0 = goto 2 ) & ( i <> halt SCM+FSA implies (Directed (Macro i)) . 0 = i ) )
A2: (Macro i) . 0 = i by COMPOS_1:58;
0 in {0,1} by TARSKI:def 2;
then A3: 0 in dom (Macro i) by COMPOS_1:61;
A4: card (Macro i) = 2 by COMPOS_1:56;

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

A5: dom (id the InstructionsF of SCM+FSA) = the InstructionsF of SCM+FSA ;
assume A6: i = halt SCM+FSA ; :: thesis: (Directed (Macro i)) . 0 = goto 2
A7: i in dom ((halt SCM+FSA) .--> (goto 2)) by A6, TARSKI:def 1;
rng (Macro i) c= the InstructionsF of SCM+FSA by RELAT_1:def 19;
hence (Directed (Macro i)) . 0 = (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto 2))) * (Macro i)) . 0 by A4, FUNCT_7:116
.= (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) * (Macro i)) . 0 by A5, FUNCT_7:def 3
.= ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) . i by A3, A2, FUNCT_1:13
.= ((halt SCM+FSA) .--> (goto 2)) . i by A7, FUNCT_4:13
.= goto 2 by A6, FUNCOP_1:72 ;
:: thesis: verum

end;

assume i <> halt SCM+FSA ; :: thesis: (Directed (Macro i)) . 0 = i
then A9: not i in dom ((halt SCM+FSA) .--> (goto 2)) by TARSKI:def 1;
rng (Macro i) c= the InstructionsF of SCM+FSA by RELAT_1:def 19;
hence (Directed (Macro i)) . 0 = (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto 2))) * (Macro i)) . 0 by A4, FUNCT_7:116
.= (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) * (Macro i)) . 0 by A1, FUNCT_7:def 3
.= ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) . i by A3, A2, FUNCT_1:13
.= (id the InstructionsF of SCM+FSA) . i by A9, FUNCT_4:11
.= i ;
:: thesis: verum