set Mi = Macro (halt SCM+FSA );

hereby :: according to SCMFSA6B:def 4 :: thesis: Macro (halt SCM+FSA ) is parahalting

let s be State of SCM+FSA ; :: thesis: ( (Macro (halt SCM+FSA )) +* (Start-At (insloc 0 )) c= s implies for k being Element of NAT holds (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) )
assume A1: (Macro (halt SCM+FSA )) +* (Start-At (insloc 0 )) c= s ; :: thesis: for k being Element of NAT holds (Computation s,k) . (intloc 0 ) = s . (intloc 0 )
let k be Element of NAT ; :: thesis: (Computation s,k) . (intloc 0 ) = s . (intloc 0 )
A2: insloc 0 in dom ((Macro (halt SCM+FSA )) +* (Start-At (insloc 0 ))) by SCMFSA6B:31;
A3: CurInstr (Computation s,0 ) = CurInstr s by AMI_1:13
.= s . (insloc 0 ) by A1, SF_MASTR:67
.= ((Macro (halt SCM+FSA )) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A1, A2, GRFUNC_1:8
.= halt SCM+FSA by SCMFSA6B:33 ;
s = Computation s,0 by AMI_1:13;
hence (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) by A3, AMI_1:52, NAT_1:2; :: thesis: verum

end;

thus Macro (halt SCM+FSA ) is parahalting by Lm1; :: thesis: verum