theorem Th3: :: FINSEQ_5:3

for f being Function
for x, y being object st f " {y} = {x} holds
( x in dom f & y in rng f & f . x = y )