let X be set ; :: thesis: for A being Subset of REAL
for f being Function of X,REAL holds (- f) " A = f " (- A)
let A be Subset of REAL ; :: thesis: for f being Function of X,REAL holds (- f) " A = f " (- A)
let f be Function of X,REAL ; :: thesis: (- f) " A = f " (- A)

now

let x be set ; :: thesis: ( ( x in (- f) " A implies x in f " (- A) ) & ( x in f " (- A) implies x in (- f) " A ) )

hereby :: thesis: ( x in f " (- A) implies x in (- f) " A )

assume A1: x in (- f) " A ; :: thesis: x in f " (- A)
then A2: ( x in X & (- f) . x in A ) by FUNCT_2:46;
(- f) . x = - (f . x) by VALUED_1:8;
then - (- (f . x)) in - A by A2;
hence x in f " (- A) by A1, FUNCT_2:46; :: thesis: verum

end;

assume A3: x in f " (- A) ; :: thesis: x in (- f) " A
then A4: ( x in X & f . x in - A ) by FUNCT_2:46;
(- f) . x = - (f . x) by VALUED_1:8;
then (- f) . x in - (- A) by A4;
hence x in (- f) " A by A3, FUNCT_2:46; :: thesis: verum

end;

hence (- f) " A = f " (- A) by TARSKI:2; :: thesis: verum