theorem Th2: :: TOPS_5:2

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