theorem Th4: :: SCMBSORT:5

for s being State of SCM+FSA
for m, n being Nat
for a being Int-Location st m <> n + 1 holds
(Exec (((intloc m) := a),(Initialized s))) . (intloc (n + 1)) = s . (intloc (n + 1))