theorem :: SF_MASTR:46

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