let X, Y be set ; :: thesis: UsedI*Loc (X \/ Y) = () \/ ()
thus UsedI*Loc (X \/ Y) c= () \/ () :: according to XBOOLE_0:def 10 :: thesis: () \/ () c= UsedI*Loc (X \/ Y)
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in UsedI*Loc (X \/ Y) or e in () \/ () )
assume e in UsedI*Loc (X \/ Y) ; :: thesis: e in () \/ ()
then consider B being set such that
A1: e in B and
A2: B in { () 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 ) )
per cases ( i in X or i in Y ) by ;
case i in X ; :: thesis:
then B in { () where j is Instruction of SCM+FSA : j in X } by A3;
hence e in UsedI*Loc X by ; :: thesis: verum
end;
case i in Y ; :: thesis:
then B in { () where j is Instruction of SCM+FSA : j in Y } by A3;
hence e in UsedI*Loc Y by ; :: thesis: verum
end;
end;
end;
hence e in () \/ () by XBOOLE_0:def 3; :: thesis: verum
end;
( X c= X \/ Y & Y c= X \/ Y ) by XBOOLE_1:7;
then ( UsedI*Loc X c= UsedI*Loc (X \/ Y) & UsedI*Loc Y c= UsedI*Loc (X \/ Y) ) by Lm5;
hence (UsedI*Loc X) \/ () c= UsedI*Loc (X \/ Y) by XBOOLE_1:8; :: thesis: verum