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

proof

assume A1: (id X) * (R \ (id X)) = {} ; :: thesis: dom (R \ (id X)) = (dom R) \ (dom (id X))
A2: (dom R) \ (dom (id X)) c= dom (R \ (id X)) by RELAT_1:15;
for x being set st x in dom (R \ (id X)) holds
x in (dom R) \ (dom (id X))

proof

let x be set ; :: thesis: ( x in dom (R \ (id X)) implies x in (dom R) \ (dom (id X)) )
assume x in dom (R \ (id X)) ; :: thesis: x in (dom R) \ (dom (id X))
then consider y being set such that
A3: [x,y] in R \ (id X) by RELAT_1:def 4;
A4: ( [x,y] in R & not [x,y] in id X ) by A3, XBOOLE_0:def 5;
A5: ( x in dom R & not x in X implies x in (dom R) \ (dom (id X)) )

proof

assume ( x in dom R & not x in X ) ; :: thesis: x in (dom R) \ (dom (id X))
then ( x in dom R & not x in dom (id X) ) by RELAT_1:71;
hence x in (dom R) \ (dom (id X)) by XBOOLE_0:def 5; :: thesis: verum

end;

( x in dom R & not x = y implies x in (dom R) \ (dom (id X)) )

proof

not x in X

proof

assume x in X ; :: thesis: contradiction
then ( [x,x] in id X & [x,y] in R \ (id X) ) by A3, RELAT_1:def 10;
hence contradiction by A1, RELAT_1:def 8; :: thesis: verum

end;

hence ( x in dom R & not x = y implies x in (dom R) \ (dom (id X)) ) by A5; :: thesis: verum

end;

hence x in (dom R) \ (dom (id X)) by A4, A5, RELAT_1:def 4, RELAT_1:def 10; :: thesis: verum

end;

then dom (R \ (id X)) c= (dom R) \ (dom (id X)) by TARSKI:def 3;
hence dom (R \ (id X)) = (dom R) \ (dom (id X)) by A2, XBOOLE_0:def 10; :: thesis: verum

end;

thus ( (R \ (id X)) * (id X) = {} implies rng (R \ (id X)) = (rng R) \ (rng (id X)) ) :: thesis: verum

proof

assume A6: (R \ (id X)) * (id X) = {} ; :: thesis: rng (R \ (id X)) = (rng R) \ (rng (id X))
A7: (rng R) \ (rng (id X)) c= rng (R \ (id X)) by RELAT_1:28;
rng (R \ (id X)) c= (rng R) \ (rng (id X))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (R \ (id X)) or y in (rng R) \ (rng (id X)) )
assume y in rng (R \ (id X)) ; :: thesis: y in (rng R) \ (rng (id X))
then consider x being set such that
A8: [x,y] in R \ (id X) by RELAT_1:def 5;
A9: ( [x,y] in R & not [x,y] in id X ) by A8, XBOOLE_0:def 5;
A10: ( y in rng R & not y in X implies y in (rng R) \ (rng (id X)) )

proof

assume ( y in rng R & not y in X ) ; :: thesis: y in (rng R) \ (rng (id X))
then ( y in rng R & not y in rng (id X) ) by RELAT_1:71;
hence y in (rng R) \ (rng (id X)) by XBOOLE_0:def 5; :: thesis: verum

end;

( y in rng R & not x = y implies y in (rng R) \ (rng (id X)) )

proof

not y in X

proof

assume y in X ; :: thesis: contradiction
then ( [y,y] in id X & [x,y] in R \ (id X) ) by A8, RELAT_1:def 10;
hence contradiction by A6, RELAT_1:def 8; :: thesis: verum

end;

hence ( y in rng R & not x = y implies y in (rng R) \ (rng (id X)) ) by A10; :: thesis: verum

end;

hence y in (rng R) \ (rng (id X)) by A9, A10, RELAT_1:def 5, RELAT_1:def 10; :: thesis: verum

end;

hence rng (R \ (id X)) = (rng R) \ (rng (id X)) by A7, XBOOLE_0:def 10; :: thesis: verum

end;