theorem Th1: :: T_0TOPSP:1

for X, Y being non empty set
for f being Function of X,Y
for A being Subset of X st ( for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds
x2 in A ) holds
f " (f .: A) = A