theorem :: SF_MASTR:45

for i being Instruction of SCM+FSA
for J being Program of holds UsedI*Loc (i ";" J) = (UsedInt*Loc i) \/ (UsedI*Loc J)