theorem Th9: :: FUNCOP_1:9

for f being Function
for x being object st rng f = {x} holds
f = (dom f) --> x