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))
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)) )
A2: ( x in dom R & not x in X & x in dom (R \ (id X)) implies x in (dom R) \ (dom (id X)) )

proof

assume that
A3: x in dom R and
A4: not x in X ; :: thesis: ( not x in dom (R \ (id X)) or x in (dom R) \ (dom (id X)) )
not x in dom (id X) by A4, RELAT_1:71;
hence ( not x in dom (R \ (id X)) or x in (dom R) \ (dom (id X)) ) by A3, XBOOLE_0:def 5; :: thesis: verum

end;

assume x in dom (R \ (id X)) ; :: thesis: x in (dom R) \ (dom (id X))
then A5: ex y being set st [x,y] in R \ (id X) by RELAT_1:def 4;
not x in X

proof

assume x in X ; :: thesis: contradiction
then [x,x] in id X by RELAT_1:def 10;
hence contradiction by A1, A5, RELAT_1:def 8; :: thesis: verum

end;

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

end;

then ( (dom R) \ (dom (id X)) c= dom (R \ (id X)) & dom (R \ (id X)) c= (dom R) \ (dom (id X)) ) by RELAT_1:15, TARSKI:def 3;
hence dom (R \ (id X)) = (dom R) \ (dom (id X)) by 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 \ (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)) )
A8: ( y in rng R & not y in X & y in rng (R \ (id X)) implies y in (rng R) \ (rng (id X)) )

proof

assume that
A9: y in rng R and
A10: not y in X ; :: thesis: ( not y in rng (R \ (id X)) or y in (rng R) \ (rng (id X)) )
not y in rng (id X) by A10, RELAT_1:71;
hence ( not y in rng (R \ (id X)) or y in (rng R) \ (rng (id X)) ) by A9, XBOOLE_0:def 5; :: thesis: verum

end;

assume y in rng (R \ (id X)) ; :: thesis: y in (rng R) \ (rng (id X))
then A11: ex x being set st [x,y] in R \ (id X) by RELAT_1:def 5;
not y in X

proof

assume y in X ; :: thesis: contradiction
then [y,y] in id X by RELAT_1:def 10;
hence contradiction by A6, A11, RELAT_1:def 8; :: thesis: verum

end;

hence y in (rng R) \ (rng (id X)) by A11, A8, RELAT_1:def 5; :: thesis: verum

end;

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

end;