let p, r be preProgram of SCM+FSA; :: thesis: ( dom p misses dom r implies UsedILoc (p +* r) = (UsedILoc p) \/ (UsedILoc r) )
assume dom p misses dom r ; :: thesis: UsedILoc (p +* r) = (UsedILoc p) \/ (UsedILoc r)
then rng (p +* r) = (rng p) \/ (rng r) by NECKLACE:6;
then UsedILoc (p +* r) = UsedILoc ((rng p) \/ (rng r)) ;
hence UsedILoc (p +* r) = (UsedILoc p) \/ (UsedILoc r) by Lm3; :: thesis: verum