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)) = {} & 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 & [z,y] in R \ (id (rng R)) ) by A3, RELAT_1:def 8;
A5: z in rng R by A4, RELAT_1:20;
( [z,y] in R & not [z,y] in id (rng R) ) by A4, XBOOLE_0:def 5;
then ( [z,y] in R & z <> y ) by A5, RELAT_1:def 10;
then ( [z,y] in R & not [z,y] in id X ) by RELAT_1:def 10;
then [z,y] in R \ (id X) by 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 = {} & 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)) & [z,y] in R ) by A8, RELAT_1:def 8;
( [x,z] in R & not [x,z] in id (dom R) ) by A9, XBOOLE_0:def 5;
then ( [x,z] in R & ( not z in dom R or x <> z ) ) by RELAT_1:def 10;
then ( [x,z] in R & not [x,z] in id X ) by A9, RELAT_1:20, RELAT_1:def 10;
then [x,z] in R \ (id X) by XBOOLE_0:def 5;
hence contradiction by A6, A9, RELAT_1:def 8; :: thesis: verum

end;