let i be Instruction of SCM+FSA; :: thesis: ( (Initialized (Macro i)) . 0 = i & (Initialized (Macro i)) . 1 = halt SCM+FSA )
A1: (Macro i) . 0 = i by FUNCT_4:66;
A2: (Macro i) . 1 = halt SCM+FSA by FUNCT_4:66;
A3: Macro i c= Initialized (Macro i) by SCMFSA6A:26;
0 in dom (Macro i) by Th32;
hence (Initialized (Macro i)) . 0 = i by A1, A3, GRFUNC_1:8; :: thesis: (Initialized (Macro i)) . 1 = halt SCM+FSA
1 in dom (Macro i) by Th32;
hence (Initialized (Macro i)) . 1 = halt SCM+FSA by A2, A3, GRFUNC_1:8; :: thesis: verum