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 (() .--> 1));
A1: (s +* (Initialize (() .--> 1))) . () = (Initialize (() .--> 1)) . () by
.= 1 by SCMFSA_M:12 ;
reconsider s1 = s +* (Initialize (() .--> 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 ; :: 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 (() .--> 1)) by ;
thus (IExec ((a := k),P,s)) . b = (Result ((P +* (a := k)),s1)) . b
.= s1 . b by
.= s . b by ; :: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (IExec ((a := k),P,s)) . f = s . f
( f <> intloc 0 & f <> IC ) by ;
then A5: not f in dom (Initialize (() .--> 1)) by ;
thus (IExec ((a := k),P,s)) . f = (Result ((P +* (a := k)),s1)) . f
.= s1 . f by
.= s . f by ; :: thesis: verum