let X, Y be non empty set ; :: thesis: 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
let f be Function of X,Y; :: thesis: 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
let A be Subset of X; :: thesis: ( ( for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds
x2 in A ) implies f " (f .: A) = A )
assume A1: for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds
x2 in A ; :: thesis: f " (f .: A) = A
for x being object st x in f " (f .: A) holds
x in A

proof

let x be object ; :: thesis: ( x in f " (f .: A) implies x in A )
assume A2: x in f " (f .: A) ; :: thesis: x in A
then f . x in f .: A by FUNCT_1:def 7;
then ex x0 being object st
( x0 in X & x0 in A & f . x = f . x0 ) by FUNCT_2:64;
hence x in A by A1, A2; :: thesis: verum

end;

then ( A c= f " (f .: A) & f " (f .: A) c= A ) by FUNCT_2:42, TARSKI:def 3;
hence f " (f .: A) = A by XBOOLE_0:def 10; :: thesis: verum