set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
let s be State of SCM+FSA ; :: thesis: IExec (Stop SCM+FSA ),s = (Initialize s) +* (Start-At (insloc 0 ))
set s1 = (Initialize s) +* ((Stop SCM+FSA ) +* (Start-At (insloc 0 )));
A1: s +* (Initialized (Stop SCM+FSA )) = (Initialize s) +* ((Stop SCM+FSA ) +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
then CurInstr ((Initialize s) +* ((Stop SCM+FSA ) +* (Start-At (insloc 0 )))) = ((Initialize s) +* ((Stop SCM+FSA ) +* (Start-At (insloc 0 )))) . (insloc 0 ) by FUNCT_4:26, SCMFSA6B:34
.= (Stop SCM+FSA ) . (insloc 0 ) by Th26, SCMFSA8A:15 ;
then A2: ( CurInstr ((Initialize s) +* ((Stop SCM+FSA ) +* (Start-At (insloc 0 )))) = halt SCM+FSA & (Initialize s) +* ((Stop SCM+FSA ) +* (Start-At (insloc 0 ))) = Computation ((Initialize s) +* ((Stop SCM+FSA ) +* (Start-At (insloc 0 )))),0 ) by AMI_1:13, SCMFSA8A:16;
then A3: (Initialize s) +* ((Stop SCM+FSA ) +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;
A4: IExec (Stop SCM+FSA ),s = (Result (s +* (Initialized (Stop SCM+FSA )))) +* (s | NAT ) by SCMFSA6B:def 1;
then A5: IExec (Stop SCM+FSA ),s = ((Initialize s) +* ((Stop SCM+FSA ) +* (Start-At (insloc 0 )))) +* (s | NAT ) by A1, A2, A3, AMI_1:def 22;
then A6: DataPart (IExec (Stop SCM+FSA ),s) = DataPart ((Initialize s) +* ((Stop SCM+FSA ) +* (Start-At (insloc 0 )))) by Th37
.= DataPart (Initialize s) by SCMFSA8A:11 ;

hereby :: thesis: verum

A7: dom (IExec (Stop SCM+FSA ),s) = the carrier of SCM+FSA by AMI_1:79
.= dom ((Initialize s) +* (Start-At (insloc 0 ))) by AMI_1:79 ;
A8: dom (Start-At (insloc 0 )) = {(IC SCM+FSA )} by FUNCOP_1:19;

now

let x be set ; :: thesis: ( x in dom (IExec (Stop SCM+FSA ),s) implies (IExec (Stop SCM+FSA ),s) . b₁ = ((Initialize s) +* (Start-At (insloc 0 ))) . b₁ )
assume A9: x in dom (IExec (Stop SCM+FSA ),s) ; :: thesis: (IExec (Stop SCM+FSA ),s) . b₁ = ((Initialize s) +* (Start-At (insloc 0 ))) . b₁

per cases ( x is Int-Location or x is FinSeq-Location or x = IC SCM+FSA or x is Instruction-Location of SCM+FSA ) by A9, SCMFSA6A:35;

suppose A10: x is Int-Location ; :: thesis: (IExec (Stop SCM+FSA ),s) . b₁ = ((Initialize s) +* (Start-At (insloc 0 ))) . b₁

then A11: (IExec (Stop SCM+FSA ),s) . x = (Initialize s) . x by A6, SCMFSA6A:38;
x <> IC SCM+FSA by A10, SCMFSA_2:81;
then not x in dom (Start-At (insloc 0 )) by A8, TARSKI:def 1;
hence (IExec (Stop SCM+FSA ),s) . x = ((Initialize s) +* (Start-At (insloc 0 ))) . x by A11, FUNCT_4:12; :: thesis: verum

end;

suppose A12: x is FinSeq-Location ; :: thesis: (IExec (Stop SCM+FSA ),s) . b₁ = ((Initialize s) +* (Start-At (insloc 0 ))) . b₁

then A13: (IExec (Stop SCM+FSA ),s) . x = (Initialize s) . x by A6, SCMFSA6A:38;
x <> IC SCM+FSA by A12, SCMFSA_2:82;
then not x in dom (Start-At (insloc 0 )) by A8, TARSKI:def 1;
hence (IExec (Stop SCM+FSA ),s) . x = ((Initialize s) +* (Start-At (insloc 0 ))) . x by A13, FUNCT_4:12; :: thesis: verum

end;

suppose A14: x = IC SCM+FSA ; :: thesis: (IExec (Stop SCM+FSA ),s) . b₁ = ((Initialize s) +* (Start-At (insloc 0 ))) . b₁

then x in {(IC SCM+FSA )} by TARSKI:def 1;
then A15: x in dom (Start-At (insloc 0 )) by FUNCOP_1:19;

now

assume A16: x in NAT ; :: thesis: contradiction
then reconsider x = x as Instruction-Location of SCM+FSA by AMI_1:def 4;
x in NAT by A16;
hence contradiction by A14, AMI_1:48; :: thesis: verum

end;

then not x in (dom s) /\ NAT by XBOOLE_0:def 4;
then ( x in dom ((Initialize s) +* ((Stop SCM+FSA ) +* (Start-At (insloc 0 )))) & not x in dom (s | NAT ) ) by A14, RELAT_1:90, SCMFSA8B:1;
hence (IExec (Stop SCM+FSA ),s) . x = ((Initialize s) +* ((Stop SCM+FSA ) +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by A5, A14, FUNCT_4:12
.= (((Initialize s) +* (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by FUNCT_4:15
.= (Start-At (insloc 0 )) . (IC SCM+FSA ) by A14, A15, FUNCT_4:14
.= ((Initialize s) +* (Start-At (insloc 0 ))) . x by A14, A15, FUNCT_4:14 ;
:: thesis: verum

end;

suppose A17: x is Instruction-Location of SCM+FSA ; :: thesis: (IExec (Stop SCM+FSA ),s) . b₁ = ((Initialize s) +* (Start-At (insloc 0 ))) . b₁

(IExec (Stop SCM+FSA ),s) | NAT = s | NAT by A4, CARD_3:99
.= (Initialize s) | NAT by Th36 ;
then A18: (IExec (Stop SCM+FSA ),s) . x = (Initialize s) . x by A17, SCMFSA6A:36;
x <> IC SCM+FSA by A17, AMI_1:48;
then not x in dom (Start-At (insloc 0 )) by A8, TARSKI:def 1;
hence (IExec (Stop SCM+FSA ),s) . x = ((Initialize s) +* (Start-At (insloc 0 ))) . x by A18, FUNCT_4:12; :: thesis: verum

end;

end;

end;

hence IExec (Stop SCM+FSA ),s = (Initialize s) +* (Start-At (insloc 0 )) by A7, FUNCT_1:9; :: thesis: verum

end;