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