theorem Th9: :: SCMBSORT:10

for p being preProgram of SCM+FSA
for ic being Instruction of SCM+FSA
for fa being FinSeq-Location
for a, b being Int-Location st ic in rng p & ( ic = b := (fa,a) or ic = (fa,a) := b ) holds
fa in UsedI*Loc p