let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for a being read-write Int-Location
for k being Integer holds
( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) )
let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for k being Integer holds
( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) )
let a be read-write Int-Location ; :: thesis: for k being Integer holds
( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) )
let k be Integer; :: thesis: ( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) )
set s1 = s +* (Initialize ((intloc 0) .--> 1));
ZA: Initialize ((intloc 0) .--> 1) c= Initialized (a := k) 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 (a := k)) . (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: a := k c= P +* (a := k) by FUNCT_4:26;
not a in NAT by SCMFSA_2:84;
then not a in dom (ProgramPart s) by COMPOS_1:34;
hence (IExec ((a := k),P,s)) . a = (Result ((P +* (a := k)),s1)) . a by FUNCT_4:12
.= k by A1, A2, SCMFSA_7:38 ;
:: thesis: ( ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) )
ll: dom (Initialize ((intloc 0) .--> 1)) c= dom (Initialized (a := k)) by ZA, RELAT_1:25;

hereby :: thesis: for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f

let b be read-write Int-Location ; :: thesis: ( b <> a implies (IExec ((a := k),P,s)) . b = s . b )
assume A3: b <> a ; :: thesis: (IExec ((a := k),P,s)) . b = s . b
not b in dom (Initialized (a := k)) by SCMFSA6A:48;
then B4: not b in dom (Initialize ((intloc 0) .--> 1)) by ll;
not b in NAT by SCMFSA_2:84;
then not b in dom (ProgramPart s) by COMPOS_1:34;
hence (IExec ((a := k),P,s)) . b = (Result ((P +* (a := k)),s1)) . b by FUNCT_4:12
.= s1 . b by A1, A2, A3, SCMFSA_7:38
.= s . b by B4, FUNCT_4:12 ;
:: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (IExec ((a := k),P,s)) . f = s . f
not f in dom (Initialized (a := k)) by SCMFSA6A:49;
then B5: not f in dom (Initialize ((intloc 0) .--> 1)) by ll;
not f in NAT by SCMFSA_2:85;
then not f in dom (ProgramPart s) by COMPOS_1:34;
hence (IExec ((a := k),P,s)) . f = (Result ((P +* (a := k)),s1)) . f by FUNCT_4:12
.= s1 . f by A1, A2, SCMFSA_7:38
.= s . f by B5, FUNCT_4:12 ;
:: thesis: verum