let p, r be preProgram of SCM+FSA; :: thesis: ( dom p misses dom r implies UsedInt*Loc (p +* r) = (UsedInt*Loc p) \/ (UsedInt*Loc r) )
consider UIL being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) such that
A1: for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i and
A2: UsedInt*Loc (p +* r) = Union (UIL * (p +* r)) by Def4;
assume dom p misses dom r ; :: thesis: UsedInt*Loc (p +* r) = (UsedInt*Loc p) \/ (UsedInt*Loc r)
then ( dom (UIL * p) c= dom p & dom p misses dom (UIL * r) ) by RELAT_1:25, XBOOLE_1:63;
then A3: (UIL * p) +* (UIL * r) = (UIL * p) \/ (UIL * r) by FUNCT_4:31, XBOOLE_1:63;
dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
then rng r c= dom UIL by RELAT_1:def 19;
then UIL * (p +* r) = (UIL * p) +* (UIL * r) by FUNCT_7:9;
then A4: ( Union (UIL * r) = union (rng (UIL * r)) & union (rng (UIL * (p +* r))) = union ((rng (UIL * p)) \/ (rng (UIL * r))) ) by A3, CARD_3:def 4, RELAT_1:12;
consider UIL1 being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) such that
A5: for i being Instruction of SCM+FSA holds UIL1 . i = UsedInt*Loc i and
A6: UsedInt*Loc p = Union (UIL1 * p) by Def4;
for c being Element of the Instructions of SCM+FSA holds UIL . c = UIL1 . c

proof

let c be Element of the Instructions of SCM+FSA; :: thesis: UIL . c = UIL1 . c
reconsider d = c as Instruction of SCM+FSA ;
thus UIL . c = UsedInt*Loc d by A1
.= UIL1 . c by A5 ; :: thesis: verum

end;

then A7: UIL = UIL1 by FUNCT_2:63;
consider UIL2 being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) such that
A8: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and
A9: UsedInt*Loc r = Union (UIL2 * r) by Def4;
for c being Element of the Instructions of SCM+FSA holds UIL . c = UIL2 . c

proof

let c be Element of the Instructions of SCM+FSA; :: thesis: UIL . c = UIL2 . c
reconsider d = c as Instruction of SCM+FSA ;
thus UIL . c = UsedInt*Loc d by A1
.= UIL2 . c by A8 ; :: thesis: verum

end;

then A10: UIL = UIL2 by FUNCT_2:63;
( Union (UIL * (p +* r)) = union (rng (UIL * (p +* r))) & Union (UIL * p) = union (rng (UIL * p)) ) by CARD_3:def 4;
hence UsedInt*Loc (p +* r) = (UsedInt*Loc p) \/ (UsedInt*Loc r) by A2, A6, A9, A7, A10, A4, ZFMISC_1:78; :: thesis: verum