let X, Y be set ; :: thesis:
thus UsedILoc (X \/ Y) c= (UsedILoc X) \/ (UsedILoc Y) :: according to XBOOLE_0:def 10 :: thesis:

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in UsedILoc (X \/ Y) ; :: thesis:
then consider B being set such that
A1: e in B and
A2: B in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X \/ Y } by TARSKI:def 4;
consider i being Instruction of SCM+FSA such that
A3: B = UsedIntLoc i and
A4: i in X \/ Y by A2;

per cases by A4, XBOOLE_0:def 3;

case i in X ; :: thesis:

then B in { (UsedIntLoc j) where j is Instruction of SCM+FSA : j in X } by A3;
hence e in UsedILoc X by A1, TARSKI:def 4; :: thesis:

end;

case i in Y ; :: thesis:

then B in { (UsedIntLoc j) where j is Instruction of SCM+FSA : j in Y } by A3;
hence e in UsedILoc Y by A1, TARSKI:def 4; :: thesis:

end;

end;

end;

hence e in (UsedILoc X) \/ (UsedILoc Y) by XBOOLE_0:def 3; :: thesis:

end;

( X c= X \/ Y & Y c= X \/ Y ) by XBOOLE_1:7;
then ( UsedILoc X c= UsedILoc (X \/ Y) & UsedILoc Y c= UsedILoc (X \/ Y) ) by Lm2;
hence (UsedILoc X) \/ (UsedILoc Y) c= UsedILoc (X \/ Y) by XBOOLE_1:8; :: thesis: