theorem Th4: :: SFMASTR3:5

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