theorem Th1: :: FINTOPO5:1

for X being set
for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
(f ") .: (f .: A) = A