let P, R be Relation; :: thesis: ( rng R misses dom P implies R * P = {} )
assume A1: (rng R) /\ (dom P) = {} ; :: according to XBOOLE_0:def 7 :: thesis: R * P = {}
assume R * P <> {} ; :: thesis: contradiction
then consider x, z being object such that
A2: [x,z] in R * P ;
consider y being object such that
A3: ( [x,y] in R & [y,z] in P ) by A2, Def6;
( y in rng R & y in dom P ) by A3, XTUPLE_0:def 12, XTUPLE_0:def 13;
hence contradiction by A1, XBOOLE_0:def 4; :: thesis: verum