let p, r be preProgram of SCM+FSA; :: thesis: UsedILoc (p +* r) c= (UsedILoc p) \/ (UsedILoc r)
rng (p +* r) c= (rng p) \/ (rng r) by FUNCT_4:17;
then UsedILoc (p +* r) c= UsedILoc ((rng p) \/ (rng r)) by Lm2;
hence UsedILoc (p +* r) c= (UsedILoc p) \/ (UsedILoc r) by Lm3; :: thesis: verum