theorem :: SF_MASTR:20

for p, r being preProgram of SCM+FSA holds UsedILoc (p +* r) c= (UsedILoc p) \/ (UsedILoc r)