let p, r be preProgram of SCM+FSA ; :: thesis: UsedIntLoc (p +* r) c= (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 ) & UsedIntLoc (p +* r) = Union (UIL * (p +* r)) ) by Def2;
consider UIL1 being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that
A2: ( ( for i being Instruction of SCM+FSA holds UIL1 . i = UsedIntLoc i ) & UsedIntLoc p = Union (UIL1 * p) ) by Def2;
consider UIL2 being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that
A3: ( ( for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i ) & UsedIntLoc r = Union (UIL2 * r) ) 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 A2 ; :: thesis: verum

end;

then A4: UIL = UIL1 by FUNCT_2:113;
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 A3 ; :: thesis: verum

end;

then A5: UIL = UIL2 by FUNCT_2:113;
A6: Union (UIL * (p +* r)) = union (rng (UIL * (p +* r))) by CARD_3:def 4;
A7: Union (UIL * p) = union (rng (UIL * p)) by CARD_3:def 4;
A8: Union (UIL * r) = union (rng (UIL * r)) by CARD_3:def 4;
dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
then ( rng p c= dom UIL & rng r c= dom UIL ) by AMI_1:118;
then UIL * (p +* r) = (UIL * p) +* (UIL * r) by FUNCT_7:10;
then union (rng (UIL * (p +* r))) c= union ((rng (UIL * p)) \/ (rng (UIL * r))) by FUNCT_4:18, ZFMISC_1:95;
hence UsedIntLoc (p +* r) c= (UsedIntLoc p) \/ (UsedIntLoc r) by A1, A2, A3, A4, A5, A6, A7, A8, ZFMISC_1:96; :: thesis: verum