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

hence f " (f .: A) = A by XBOOLE_0:def 10; :: thesis: verum

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

then
( A c= f " (f .: A) & f " (f .: A) c= A )
by FUNCT_2:42, TARSKI:def 3;
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;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

hence f " (f .: A) = A by XBOOLE_0:def 10; :: thesis: verum