let s be State of SCM+FSA; :: thesis: IExec ((Stop SCM+FSA),s) = (Initialized s) +* (Start-At (0,SCM+FSA))
set D = Int-Locations \/ FinSeq-Locations;
set A = NAT ;
set s1 = (Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA)));
A1: (Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA))) = Comput ((ProgramPart ((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA)))),0) by EXTPRO_1:3;
A2: IExec ((Stop SCM+FSA),s) = (Result ((ProgramPart (s +* (Initialized (Stop SCM+FSA)))),(s +* (Initialized (Stop SCM+FSA))))) +* (s | NAT) by SCMFSA6B:def 1;
Y: (ProgramPart ((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA))))) /. (IC ((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA))))) = ((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA)))) . (IC ((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA))))) by COMPOS_1:38;
y: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:38;
x: 0 in dom (Stop SCM+FSA) by COMPOS_1:45;
A3: s +* (Initialized (Stop SCM+FSA)) = (Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA))) by SCMFSA8A:13;
then A4: CurInstr ((ProgramPart ((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA))))) = ((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA)))) . 0 by Y, FUNCT_4:26, SCMFSA6B:34
.= (Stop SCM+FSA) . 0 by Th26, x ;
then ProgramPart ((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA)))) halts_on (Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA))) by A1, y, EXTPRO_1:30;
then A5: IExec ((Stop SCM+FSA),s) = ((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA)))) +* (s | NAT) by A3, A4, A1, A2, y, EXTPRO_1:def 8;
then A6: DataPart (IExec ((Stop SCM+FSA),s)) = DataPart ((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA)))) by Th37
.= DataPart (Initialized s) by SCMFSA8A:11 ;

hereby :: thesis: verum

A7: dom (Start-At (0,SCM+FSA)) = {(IC SCM+FSA)} by FUNCOP_1:19;

A8: now

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

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

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

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

end;

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

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

end;

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

then x in {(IC SCM+FSA)} by TARSKI:def 1;
then A15: x in dom (Start-At (0,SCM+FSA)) by FUNCOP_1:19;
not x in NAT by A14, COMPOS_1:3;
then not x in (dom s) /\ NAT by XBOOLE_0:def 4;
then not x in dom (s | NAT) by RELAT_1:90;
hence (IExec ((Stop SCM+FSA),s)) . x = ((Initialized s) +* ((Stop SCM+FSA) +* (Start-At (0,SCM+FSA)))) . (IC SCM+FSA) by A5, A14, FUNCT_4:12
.= (((Initialized s) +* (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) . (IC SCM+FSA) by FUNCT_4:15
.= (Start-At (0,SCM+FSA)) . (IC SCM+FSA) by A14, A15, FUNCT_4:14
.= ((Initialized s) +* (Start-At (0,SCM+FSA))) . x by A14, A15, FUNCT_4:14 ;
:: thesis: verum

end;

suppose A17: x is Element of NAT ; :: thesis: (IExec ((Stop SCM+FSA),s)) . b₁ = ((Initialized s) +* (Start-At (0,SCM+FSA))) . b₁

then x <> IC SCM+FSA by COMPOS_1:3;
then A18: not x in dom (Start-At (0,SCM+FSA)) by A7, TARSKI:def 1;
(IExec ((Stop SCM+FSA),s)) | NAT = s | NAT by A2, PBOOLE:157
.= (Initialized s) | NAT by Th36 ;
then (IExec ((Stop SCM+FSA),s)) . x = (Initialized s) . x by A17, SCMFSA6A:36;
hence (IExec ((Stop SCM+FSA),s)) . x = ((Initialized s) +* (Start-At (0,SCM+FSA))) . x by A18, FUNCT_4:12; :: thesis: verum

end;

end;

end;

dom (IExec ((Stop SCM+FSA),s)) = the carrier of SCM+FSA by PARTFUN1:def 4
.= dom ((Initialized s) +* (Start-At (0,SCM+FSA))) by PARTFUN1:def 4 ;
hence IExec ((Stop SCM+FSA),s) = (Initialized s) +* (Start-At (0,SCM+FSA)) by A8, FUNCT_1:9; :: thesis: verum

end;