let X, Y be set ; :: thesis: UsedI*Loc (X \/ Y) = (UsedI*Loc X) \/ (UsedI*Loc Y)

thus UsedI*Loc (X \/ Y) c= (UsedI*Loc X) \/ (UsedI*Loc Y) :: according to XBOOLE_0:def 10 :: thesis: (UsedI*Loc X) \/ (UsedI*Loc Y) c= UsedI*Loc (X \/ Y)

then ( UsedI*Loc X c= UsedI*Loc (X \/ Y) & UsedI*Loc Y c= UsedI*Loc (X \/ Y) ) by Lm5;

hence (UsedI*Loc X) \/ (UsedI*Loc Y) c= UsedI*Loc (X \/ Y) by XBOOLE_1:8; :: thesis: verum

thus UsedI*Loc (X \/ Y) c= (UsedI*Loc X) \/ (UsedI*Loc Y) :: according to XBOOLE_0:def 10 :: thesis: (UsedI*Loc X) \/ (UsedI*Loc Y) c= UsedI*Loc (X \/ Y)

proof

( X c= X \/ Y & Y c= X \/ Y )
by XBOOLE_1:7;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in UsedI*Loc (X \/ Y) or e in (UsedI*Loc X) \/ (UsedI*Loc Y) )

assume e in UsedI*Loc (X \/ Y) ; :: thesis: e in (UsedI*Loc X) \/ (UsedI*Loc Y)

then consider B being set such that

A1: e in B and

A2: B in { (UsedInt*Loc 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 = UsedInt*Loc i and

A4: i in X \/ Y by A2;

end;assume e in UsedI*Loc (X \/ Y) ; :: thesis: e in (UsedI*Loc X) \/ (UsedI*Loc Y)

then consider B being set such that

A1: e in B and

A2: B in { (UsedInt*Loc 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 = UsedInt*Loc i and

A4: i in X \/ Y by A2;

now :: thesis: ( ( i in X & e in UsedI*Loc X ) or ( i in Y & e in UsedI*Loc Y ) )end;

hence
e in (UsedI*Loc X) \/ (UsedI*Loc Y)
by XBOOLE_0:def 3; :: thesis: verumper cases
( i in X or i in Y )
by A4, XBOOLE_0:def 3;

end;

case
i in X
; :: thesis: e in UsedI*Loc X

then
B in { (UsedInt*Loc j) where j is Instruction of SCM+FSA : j in X }
by A3;

hence e in UsedI*Loc X by A1, TARSKI:def 4; :: thesis: verum

end;hence e in UsedI*Loc X by A1, TARSKI:def 4; :: thesis: verum

case
i in Y
; :: thesis: e in UsedI*Loc Y

then
B in { (UsedInt*Loc j) where j is Instruction of SCM+FSA : j in Y }
by A3;

hence e in UsedI*Loc Y by A1, TARSKI:def 4; :: thesis: verum

end;hence e in UsedI*Loc Y by A1, TARSKI:def 4; :: thesis: verum

then ( UsedI*Loc X c= UsedI*Loc (X \/ Y) & UsedI*Loc Y c= UsedI*Loc (X \/ Y) ) by Lm5;

hence (UsedI*Loc X) \/ (UsedI*Loc Y) c= UsedI*Loc (X \/ Y) by XBOOLE_1:8; :: thesis: verum