let i be Instruction of SCM+FSA ; ( (Macro i) . 0 = i & (Macro i) . 1 = halt SCM+FSA & (Initialized (Macro i)) . 0 = i & (Initialized (Macro i)) . 1 = halt SCM+FSA & ((Macro i) +* (Start-At 0 ,SCM+FSA )) . 0 = i )
thus A1:
(Macro i) . 0 = i
by FUNCT_4:66; ( (Macro i) . 1 = halt SCM+FSA & (Initialized (Macro i)) . 0 = i & (Initialized (Macro i)) . 1 = halt SCM+FSA & ((Macro i) +* (Start-At 0 ,SCM+FSA )) . 0 = i )
thus A2:
(Macro i) . 1 = halt SCM+FSA
by FUNCT_4:66; ( (Initialized (Macro i)) . 0 = i & (Initialized (Macro i)) . 1 = halt SCM+FSA & ((Macro i) +* (Start-At 0 ,SCM+FSA )) . 0 = i )
A3:
Macro i c= Initialized (Macro i)
by SCMFSA6A:26;
A4:
0 in dom (Macro i)
by Th32;
hence
(Initialized (Macro i)) . 0 = i
by A1, A3, GRFUNC_1:8; ( (Initialized (Macro i)) . 1 = halt SCM+FSA & ((Macro i) +* (Start-At 0 ,SCM+FSA )) . 0 = i )
1 in dom (Macro i)
by Th32;
hence
(Initialized (Macro i)) . 1 = halt SCM+FSA
by A2, A3, GRFUNC_1:8; ((Macro i) +* (Start-At 0 ,SCM+FSA )) . 0 = i
dom (Macro i) misses dom (Start-At 0 ,SCM+FSA )
by SF_MASTR:64;
then
Macro i c= (Macro i) +* (Start-At 0 ,SCM+FSA )
by FUNCT_4:33;
hence
((Macro i) +* (Start-At 0 ,SCM+FSA )) . 0 = i
by A1, A4, GRFUNC_1:8; verum