let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA holds IExec ((Stop SCM+FSA),P,s) = Initialize (Initialized s)
let s be State of SCM+FSA; :: thesis: IExec ((Stop SCM+FSA),P,s) = Initialize (Initialized s)
set D = Data-Locations SCM+FSA;
set A = NAT ;
set s1 = (Initialized s) +* (Initialize (Stop SCM+FSA));
set P1 = P +* (Stop SCM+FSA);
A1: Stop SCM+FSA c= P +* (Stop SCM+FSA) by FUNCT_4:26;
A2: (Initialized s) +* (Initialize (Stop SCM+FSA)) = Comput ((P +* (Stop SCM+FSA)),((Initialized s) +* (Initialize (Stop SCM+FSA))),0) by EXTPRO_1:3;
A3: (P +* (Stop SCM+FSA)) /. (IC ((Initialized s) +* (Initialize (Stop SCM+FSA)))) = (P +* (Stop SCM+FSA)) . (IC ((Initialized s) +* (Initialize (Stop SCM+FSA)))) by PBOOLE:158;
A4: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:38;
A5: 0 in dom (Stop SCM+FSA) by COMPOS_1:45;
A6: s +* (Initialized (Stop SCM+FSA)) = (Initialized s) +* (Initialize (Stop SCM+FSA)) by SCMFSA8A:13;
then A7: CurInstr ((P +* (Stop SCM+FSA)),((Initialized s) +* (Initialize (Stop SCM+FSA)))) = (P +* (Stop SCM+FSA)) . 0 by A3, FUNCT_4:26, SCMFSA6B:34
.= (Stop SCM+FSA) . 0 by A5, A1, GRFUNC_1:8 ;
then P +* (Stop SCM+FSA) halts_on (Initialized s) +* (Initialize (Stop SCM+FSA)) by A2, A4, EXTPRO_1:30;
then A8: IExec ((Stop SCM+FSA),P,s) = ((Initialized s) +* (Initialize (Stop SCM+FSA))) +* (s | NAT) by A6, A7, A2, A4, EXTPRO_1:def 8;
then A9: DataPart (IExec ((Stop SCM+FSA),P,s)) = DataPart ((Initialized s) +* (Initialize (Stop SCM+FSA))) by COMPOS_1:82
.= DataPart (Initialized s) by SCMFSA8A:11 ;

hereby :: thesis: verum

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

A11: now

let x be set ; :: thesis: ( x in dom (IExec ((Stop SCM+FSA),P,s)) implies (IExec ((Stop SCM+FSA),P,s)) . b₁ = (Initialize (Initialized s)) . b₁ )
assume A12: x in dom (IExec ((Stop SCM+FSA),P,s)) ; :: thesis: (IExec ((Stop SCM+FSA),P,s)) . b₁ = (Initialize (Initialized s)) . b₁

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

suppose A13: x is Int-Location ; :: thesis: (IExec ((Stop SCM+FSA),P,s)) . b₁ = (Initialize (Initialized s)) . b₁

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

end;

suppose A15: x is FinSeq-Location ; :: thesis: (IExec ((Stop SCM+FSA),P,s)) . b₁ = (Initialize (Initialized s)) . b₁

then x <> IC by SCMFSA_2:82;
then A16: not x in dom (Start-At (0,SCM+FSA)) by A10, TARSKI:def 1;
(IExec ((Stop SCM+FSA),P,s)) . x = (Initialized s) . x by A9, A15, SCMFSA6A:38;
hence (IExec ((Stop SCM+FSA),P,s)) . x = (Initialize (Initialized s)) . x by A16, FUNCT_4:12; :: thesis: verum

end;

suppose A17: x = IC ; :: thesis: (IExec ((Stop SCM+FSA),P,s)) . b₁ = (Initialize (Initialized s)) . b₁

then x in {(IC )} by TARSKI:def 1;
then A18: x in dom (Start-At (0,SCM+FSA)) by FUNCOP_1:19;
not x in dom (s | NAT) by A17, COMPOS_1:139;
hence (IExec ((Stop SCM+FSA),P,s)) . x = ((Initialized s) +* (Initialize (Stop SCM+FSA))) . (IC ) by A8, A17, FUNCT_4:12
.= (Initialize ((Initialized s) +* (Stop SCM+FSA))) . (IC ) by FUNCT_4:15
.= (Start-At (0,SCM+FSA)) . (IC ) by A17, A18, FUNCT_4:14
.= (Initialize (Initialized s)) . x by A17, A18, FUNCT_4:14 ;
:: thesis: verum

end;

suppose A19: x is Element of NAT ; :: thesis: (IExec ((Stop SCM+FSA),P,s)) . b₁ = (Initialize (Initialized s)) . b₁

then x <> IC by COMPOS_1:3;
then A20: not x in dom (Start-At (0,SCM+FSA)) by A10, TARSKI:def 1;
dom (ProgramPart s) = NAT by COMPOS_1:34;
then x in dom (ProgramPart s) by A19;
hence (IExec ((Stop SCM+FSA),P,s)) . x = (s | NAT) . x by FUNCT_4:14
.= ((Initialized s) | NAT) . x by Th36
.= (Initialized s) . x by A19, FUNCT_1:72
.= (Initialize (Initialized s)) . x by A20, FUNCT_4:12 ;
:: thesis: verum

end;

end;

end;

dom (IExec ((Stop SCM+FSA),P,s)) = the carrier of SCM+FSA by PARTFUN1:def 4
.= dom (Initialize (Initialized s)) by PARTFUN1:def 4 ;
hence IExec ((Stop SCM+FSA),P,s) = Initialize (Initialized s) by A11, FUNCT_1:9; :: thesis: verum

end;