theorem :: RELSET_1:23

for X, Y being set
for R being Relation of X,Y holds
( R .: (R " Y) = rng R & R " (R .: X) = dom R )