theorem :: FUNCT_4:112

for y, x being object
for R being Relation st dom R = {x} & rng R = {y} holds
R = x .--> y