for P being Instruction-Sequence of SCM+FSA
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 ) )