let X be set ; for R being Relation holds
( ( R * (R \ (id X)) = {} implies R * (R \ (id (rng R))) = {} ) & ( (R \ (id X)) * R = {} implies (R \ (id (dom R))) * R = {} ) )
let R be Relation; ( ( R * (R \ (id X)) = {} implies R * (R \ (id (rng R))) = {} ) & ( (R \ (id X)) * R = {} implies (R \ (id (dom R))) * R = {} ) )
thus
( R * (R \ (id X)) = {} implies R * (R \ (id (rng R))) = {} )
( (R \ (id X)) * R = {} implies (R \ (id (dom R))) * R = {} )proof
assume that A1:
R * (R \ (id X)) = {}
and A2:
R * (R \ (id (rng R))) <> {}
;
contradiction
consider x,
y being
object such that A3:
[x,y] in R * (R \ (id (rng R)))
by A2;
consider z being
object 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, XBOOLE_0:def 5, XTUPLE_0:def 13;
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;
verum
end;
assume that
A6:
(R \ (id X)) * R = {}
and
A7:
(R \ (id (dom R))) * R <> {}
; contradiction
consider x, y being object such that
A8:
[x,y] in (R \ (id (dom R))) * R
by A7;
consider z being object 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:def 10, XTUPLE_0:def 12;
then
[x,z] in R \ (id X)
by A9, XBOOLE_0:def 5;
hence
contradiction
by A6, A10, RELAT_1:def 8; verum