theorem Th22: :: RELSET_1:22

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