theorem :: SF_MASTR:36

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