theorem :: SCMFSA9A:44

for b being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedILoc (Times (b,I)) = {b,(intloc 0)} \/ (UsedILoc I)