theorem Th71: :: FUNCT_1:72

for y being object
for R being Relation holds
( y in rng R iff R " {y} <> {} )