theorem :: RELAT_1:189

for f being Relation
for x, y being object st dom f = {x} & rng f = {y} holds
f = {[x,y]}