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

proof

assume A1: (id X) * (R \ (id X)) = {} ; :: thesis: dom (R \ (id X)) = (dom R) \ X
A2: dom (R \ (id X)) c= (dom R) \ X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (R \ (id X)) or x in (dom R) \ X )
A3: ( x in dom R & not x in X & x in dom (R \ (id X)) implies x in (dom R) \ X ) by XBOOLE_0:def 5;
assume x in dom (R \ (id X)) ; :: thesis: x in (dom R) \ X
then A4: ex y being object st [x,y] in R \ (id X) by XTUPLE_0:def 12;
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, A4, RELAT_1:def 8; :: thesis: verum

end;

hence x in (dom R) \ X by A4, A3, XTUPLE_0:def 12; :: thesis: verum

end;

(dom R) \ (dom (id X)) c= dom (R \ (id X)) by XTUPLE_0:25;
then (dom R) \ X c= dom (R \ (id X)) ;
hence dom (R \ (id X)) = (dom R) \ X by A2; :: thesis: verum

end;

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

proof

assume A5: (R \ (id X)) * (id X) = {} ; :: thesis: rng (R \ (id X)) = (rng R) \ X
A6: rng (R \ (id X)) c= (rng R) \ X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (R \ (id X)) or y in (rng R) \ X )
A7: ( y in rng R & not y in X & y in rng (R \ (id X)) implies y in (rng R) \ X ) by XBOOLE_0:def 5;
assume y in rng (R \ (id X)) ; :: thesis: y in (rng R) \ X
then A8: ex x being object st [x,y] in R \ (id X) by XTUPLE_0:def 13;
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 A5, A8, RELAT_1:def 8; :: thesis: verum

end;

hence y in (rng R) \ X by A8, A7, XTUPLE_0:def 13; :: thesis: verum

end;

(rng R) \ (rng (id X)) c= rng (R \ (id X)) by RELAT_1:14;
then (rng R) \ X c= rng (R \ (id X)) ;
hence rng (R \ (id X)) = (rng R) \ X by A6; :: thesis: verum

end;