let p, r be preProgram of SCM+FSA ; :: thesis: ( dom p misses dom r implies UsedIntLoc (p +* r) = (UsedIntLoc p) \/ (UsedIntLoc r) )
consider UIL being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that
A1: for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i and
A2: UsedIntLoc (p +* r) = Union (UIL * (p +* r)) by Def2;
assume dom p misses dom r ; :: thesis: UsedIntLoc (p +* r) = (UsedIntLoc p) \/ (UsedIntLoc r)
then ( dom (UIL * p) c= dom p & dom p misses dom (UIL * r) ) by RELAT_1:44, XBOOLE_1:63;
then A3: (UIL * p) +* (UIL * r) = (UIL * p) \/ (UIL * r) by FUNCT_4:32, 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:10;
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:26;
consider UIL1 being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that
A5: for i being Instruction of SCM+FSA holds UIL1 . i = UsedIntLoc i and
A6: UsedIntLoc p = Union (UIL1 * p) by Def2;
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 = UsedIntLoc d by A1
.= UIL1 . c by A5 ; :: thesis: verum

end;

then A7: UIL = UIL1 by FUNCT_2:113;
consider UIL2 being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that
A8: for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i and
A9: UsedIntLoc r = Union (UIL2 * r) by Def2;
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 = UsedIntLoc d by A1
.= UIL2 . c by A8 ; :: thesis: verum

end;

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