let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for f being FinSeq-Location
for p being FinSequence of INT holds
( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec ((f := p),P,s)) . g = s . g ) )
let s be State of SCM+FSA; :: thesis: for f being FinSeq-Location
for p being FinSequence of INT holds
( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec ((f := p),P,s)) . g = s . g ) )
let f be FinSeq-Location ; :: thesis: for p being FinSequence of INT holds
( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec ((f := p),P,s)) . g = s . g ) )
let p be FinSequence of INT ; :: thesis: ( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec ((f := p),P,s)) . g = s . g ) )
ZA: Initialize ((intloc 0) .--> 1) c= Initialized (f := p) by FUNCT_4:26;
NA: intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:86;
then A1: (s +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) = (Initialize ((intloc 0) .--> 1)) . (intloc 0) by FUNCT_4:14
.= (Initialized (f := p)) . (intloc 0) by NA, ZA, GRFUNC_1:8
.= 1 by SCMFSA6A:46 ;
reconsider s1 = s +* (Initialize ((intloc 0) .--> 1)) as 0 -started State of SCM+FSA ;
A2: f := p c= P +* (f := p) by FUNCT_4:26;
not f in NAT by SCMFSA_2:85;
then not f in dom (ProgramPart s) by COMPOS_1:34;
hence (IExec ((f := p),P,s)) . f = (Result ((P +* (f := p)),s1)) . f by FUNCT_4:12
.= p by A1, A2, SCMFSA_7:39 ;
:: thesis: ( ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec ((f := p),P,s)) . g = s . g ) )

hereby :: thesis: for g being FinSeq-Location st g <> f holds
(IExec ((f := p),P,s)) . g = s . g

let a be read-write Int-Location ; :: thesis: ( a <> intloc 1 & a <> intloc 2 implies (IExec ((f := p),P,s)) . a = s . a )
A6: not a in dom (Initialized (f := p)) by SCMFSA6A:48;
dom (Initialize ((intloc 0) .--> 1)) c= dom (Initialized (f := p)) by ZA, RELAT_1:25;
then B6: not a in dom (Initialize ((intloc 0) .--> 1)) by A6;
assume A3: ( a <> intloc 1 & a <> intloc 2 ) ; :: thesis: (IExec ((f := p),P,s)) . a = s . a
not a in NAT by SCMFSA_2:84;
then not a in dom (ProgramPart s) by COMPOS_1:34;
hence (IExec ((f := p),P,s)) . a = (Result ((P +* (f := p)),(s +* (Initialize ((intloc 0) .--> 1))))) . a by FUNCT_4:12
.= s1 . a by A1, A2, A3, SCMFSA_7:39
.= s . a by B6, FUNCT_4:12 ;
:: thesis: verum

end;

let g be FinSeq-Location ; :: thesis: ( g <> f implies (IExec ((f := p),P,s)) . g = s . g )
assume A5: g <> f ; :: thesis: (IExec ((f := p),P,s)) . g = s . g
A6: not g in dom (Initialized (f := p)) by SCMFSA6A:49;
Initialize ((intloc 0) .--> 1) c= Initialized (f := p) by FUNCT_4:26;
then dom (Initialize ((intloc 0) .--> 1)) c= dom (Initialized (f := p)) by RELAT_1:25;
then B6: not g in dom (Initialize ((intloc 0) .--> 1)) by A6;
not g in NAT by SCMFSA_2:85;
then not g in dom (ProgramPart s) by COMPOS_1:34;
hence (IExec ((f := p),P,s)) . g = (Result ((P +* (f := p)),(s +* (Initialize ((intloc 0) .--> 1))))) . g by FUNCT_4:12
.= s1 . g by A1, A2, A5, SCMFSA_7:39
.= s . g by B6, FUNCT_4:12 ;
:: thesis: verum