let p, r be preProgram of SCM+FSA; :: thesis: UsedInt*Loc (p +* r) c= (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;
consider UIL1 being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) such that
A3: for i being Instruction of SCM+FSA holds UIL1 . i = UsedInt*Loc i and
A4: 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 A3 ; :: thesis: verum

end;

then A5: UIL = UIL1 by FUNCT_2:63;
consider UIL2 being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) such that
A6: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and
A7: 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 A6 ; :: thesis: verum

end;

then A8: UIL = UIL2 by FUNCT_2: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 A9: ( Union (UIL * r) = union (rng (UIL * r)) & union (rng (UIL * (p +* r))) c= union ((rng (UIL * p)) \/ (rng (UIL * r))) ) by CARD_3:def 4, FUNCT_4:17, ZFMISC_1:77;
( 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) c= (UsedInt*Loc p) \/ (UsedInt*Loc r) by A2, A4, A7, A5, A8, A9, ZFMISC_1:78; :: thesis: verum