theorem :: RELAT_1:44

for P, R being Relation st rng R misses dom P holds
R * P = {}