let X, Y be set ; :: thesis: for R being Relation holds
( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
let R be Relation; :: thesis: ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
per cases ( X = {} or Y = {} or ( X <> {} & Y <> {} ) ) ;
suppose ( X = {} or Y = {} ) ; :: thesis: ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
then R /\ [:X,Y:] = R /\ {} by ZFMISC_1:90
.= {} ;
hence ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y ) ; :: thesis: verum
end;
suppose A1: ( X <> {} & Y <> {} ) ; :: thesis: ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
rng (R /\ [:X,Y:]) c= (rng R) /\ (rng [:X,Y:]) by RELAT_1:13;
then A2: rng (R /\ [:X,Y:]) c= (rng R) /\ Y by A1, Lm1;
dom (R /\ [:X,Y:]) c= (dom R) /\ (dom [:X,Y:]) by XTUPLE_0:24;
then A3: dom (R /\ [:X,Y:]) c= (dom R) /\ X by A1, Lm1;
(dom R) /\ X c= X by XBOOLE_1:17;
hence dom (R /\ [:X,Y:]) c= X by A3; :: thesis: rng (R /\ [:X,Y:]) c= Y
(rng R) /\ Y c= Y by XBOOLE_1:17;
hence rng (R /\ [:X,Y:]) c= Y by A2; :: thesis: verum
end;
end;