let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA holds IExec ((Stop SCM+FSA),P,s) = Initialized s
let s be State of SCM+FSA; :: thesis: IExec ((Stop SCM+FSA),P,s) = Initialized s
set D = Data-Locations ;
set A = NAT ;
set s1 = Initialize (Initialized s);
set P1 = P +* (Stop SCM+FSA);
A1: Stop SCM+FSA c= P +* (Stop SCM+FSA) by FUNCT_4:25;
A2: Initialize (Initialized s) = Comput ((P +* (Stop SCM+FSA)),(Initialize (Initialized s)),0) by EXTPRO_1:2;
A3: (P +* (Stop SCM+FSA)) /. (IC (Initialize (Initialized s))) = (P +* (Stop SCM+FSA)) . (IC (Initialize (Initialized s))) by PBOOLE:143;
A4: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:34;
A5: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
A6: s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by MEMSTR_0:44;
A7: CurInstr ((P +* (Stop SCM+FSA)),(Initialize (Initialized s))) = (P +* (Stop SCM+FSA)) . 0 by A3, A6, FUNCT_4:25, SCMFSA6B:10
.= (Stop SCM+FSA) . 0 by A5, A1, GRFUNC_1:2 ;
then P +* (Stop SCM+FSA) halts_on Initialize (Initialized s) by A2, A4, EXTPRO_1:29;
then A8: IExec ((Stop SCM+FSA),P,s) = Initialize (Initialized s) by A6, A7, A2, A4, EXTPRO_1:def 9;
then A9: DataPart (IExec ((Stop SCM+FSA),P,s)) = DataPart (Initialize (Initialized s))
.= DataPart (Initialized s) by MEMSTR_0:79 ;

hereby :: thesis: verum

A11: now

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

per cases ( x is Int-Location or x is FinSeq-Location or x = IC ) by A12, SCMFSA6A:5;

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

(IExec ((Stop SCM+FSA),P,s)) . x = (Initialized s) . x by A9, A13, SCMFSA6A:7;
hence (IExec ((Stop SCM+FSA),P,s)) . x = (Initialized s) . x ; :: thesis: verum

end;

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

(IExec ((Stop SCM+FSA),P,s)) . x = (Initialized s) . x by A9, A15, SCMFSA6A:7;
hence (IExec ((Stop SCM+FSA),P,s)) . x = (Initialized s) . x ; :: thesis: verum

end;

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

then x in {(IC )} by TARSKI:def 1;
then A18: x in dom (Start-At (0,SCM+FSA)) by FUNCOP_1:13;
thus (IExec ((Stop SCM+FSA),P,s)) . x = (Initialize (Initialized s)) . (IC ) by A8, A17
.= (Start-At (0,SCM+FSA)) . (IC ) by A17, A18, FUNCT_4:13
.= ((s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) . x by A17, A18, FUNCT_4:13
.= (s +* (Initialize ((intloc 0) .--> 1))) . x by FUNCT_4:14
.= (Initialized s) . x ; :: thesis: verum

end;

end;

end;

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

end;