let X be set ; :: thesis: for R being Relation holds
( ( R * (R \ (id X)) = {} & rng R c= X implies R * (R \ (id (rng R))) = {} ) & ( (R \ (id X)) * R = {} & dom R c= X implies (R \ (id (dom R))) * R = {} ) )
let R be Relation; :: thesis: ( ( R * (R \ (id X)) = {} & rng R c= X implies R * (R \ (id (rng R))) = {} ) & ( (R \ (id X)) * R = {} & dom R c= X implies (R \ (id (dom R))) * R = {} ) )
thus ( R * (R \ (id X)) = {} & rng R c= X implies R * (R \ (id (rng R))) = {} ) :: thesis: ( (R \ (id X)) * R = {} & dom R c= X implies (R \ (id (dom R))) * R = {} )

proof

assume that
A1: R * (R \ (id X)) = {} and
rng R c= X and
A2: not R * (R \ (id (rng R))) = {} ; :: thesis: contradiction
consider x, y being set such that
A3: [x,y] in R * (R \ (id (rng R))) by A2, RELAT_1:56;
consider z being set such that
A4: [x,z] in R and
A5: [z,y] in R \ (id (rng R)) by A3, RELAT_1:def 8;
( z in rng R & not [z,y] in id (rng R) ) by A4, A5, RELAT_1:20, XBOOLE_0:def 5;
then z <> y by RELAT_1:def 10;
then not [z,y] in id X by RELAT_1:def 10;
then [z,y] in R \ (id X) by A5, XBOOLE_0:def 5;
hence contradiction by A1, A4, RELAT_1:def 8; :: thesis: verum

end;

thus ( (R \ (id X)) * R = {} & dom R c= X implies (R \ (id (dom R))) * R = {} ) :: thesis: verum

proof

assume that
A6: (R \ (id X)) * R = {} and
dom R c= X and
A7: not (R \ (id (dom R))) * R = {} ; :: thesis: contradiction
consider x, y being set such that
A8: [x,y] in (R \ (id (dom R))) * R by A7, RELAT_1:56;
consider z being set such that
A9: [x,z] in R \ (id (dom R)) and
A10: [z,y] in R by A8, RELAT_1:def 8;
not [x,z] in id (dom R) by A9, XBOOLE_0:def 5;
then ( not z in dom R or x <> z ) by RELAT_1:def 10;
then not [x,z] in id X by A10, RELAT_1:20, RELAT_1:def 10;
then [x,z] in R \ (id X) by A9, XBOOLE_0:def 5;
hence contradiction by A6, A10, RELAT_1:def 8; :: thesis: verum

end;