let p, r be preProgram of SCM+FSA; :: thesis: UsedI*Loc (p +* r) c= (UsedI*Loc p) \/ (UsedI*Loc r)
rng (p +* r) c= (rng p) \/ (rng r) by FUNCT_4:17;
then UsedI*Loc (p +* r) c= UsedI*Loc ((rng p) \/ (rng r)) by Lm5;
hence UsedI*Loc (p +* r) c= (UsedI*Loc p) \/ (UsedI*Loc r) by Lm6; :: thesis: verum