theorem Th1: :: TOPS_5:1

for f being one-to-one Function
for y being object st rng f = {y} holds
dom f = {((f ") . y)}