theorem Th1: :: EUCLID_7:2

for R being Relation
for Y being set st rng R c= Y holds
R " Y = dom R