theorem Th2: :: SCMFSA9A:2

for l being Nat
for i being Instruction of SCM+FSA holds UsedI*Loc (l .--> i) = UsedInt*Loc i