let P be Instruction-Sequence of SCM+FSA; :: 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));
A1: (s +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) = (Initialize ((intloc 0) .--> 1)) . (intloc 0) by FUNCT_4:13, SCMFSA_M:10
.= 1 by SCMFSA_M:12 ;
reconsider s1 = s +* (Initialize ((intloc 0) .--> 1)) as 0 -started State of SCM+FSA ;
A2: a := k c= P +* (a := k) by FUNCT_4:25;
thus (IExec ((a := k),P,s)) . a = (Result ((P +* (a := k)),s1)) . a
.= k by A1, A2, SCMFSA_7:6 ; :: 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 ) )

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
( b <> intloc 0 & b <> IC ) by SCMFSA_2:56;
then A4: not b in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def 2;
thus (IExec ((a := k),P,s)) . b = (Result ((P +* (a := k)),s1)) . b
.= s1 . b by A1, A2, A3, SCMFSA_7:6
.= s . b by A4, FUNCT_4:11 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (IExec ((a := k),P,s)) . f = s . f
( f <> intloc 0 & f <> IC ) by SCMFSA_2:57, SCMFSA_2:58;
then A5: not f in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def 2;
thus (IExec ((a := k),P,s)) . f = (Result ((P +* (a := k)),s1)) . f
.= s1 . f by A1, A2, SCMFSA_7:6
.= s . f by A5, FUNCT_4:11 ; :: thesis: verum