theorem Th2: :: SCMBSORT:3

for s being State of SCM+FSA
for f being FinSeq-Location
for a, b being Int-Location holds (Exec (((f,a) := b),s)) . f = (s . f) +* (|.(s . a).|,(s . b))