theorem Th1: :: SCMBSORT:2

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