let R, P 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 = {}

now

assume R * P <> {} ; :: thesis: contradiction
then consider x, z being set such that
A2: [x,z] in R * P by Th56;
consider y being set such that
A3: ( [x,y] in R & [y,z] in P ) by A2, Def8;
( y in rng R & y in dom P ) by A3, Def4, Def5;
hence contradiction by A1, XBOOLE_0:def 4; :: thesis: verum

end;

hence R * P = {} ; :: thesis: verum