theorem Th5: :: SFMASTR3:6

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