let X, A be set ; :: 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 x in (- f) .: A ; :: thesis: x in - (f .: A)
then consider x1 being set such that
A1: ( x1 in X & x1 in A & x = (- f) . x1 ) by FUNCT_2:115;
A2: x = - (f . x1) by A1, VALUED_1:8;
f . x1 in f .: A by A1, FUNCT_2:43;
hence x in - (f .: A) by A2; :: thesis: verum

end;

assume x in - (f .: A) ; :: thesis: x in (- f) .: A
then consider r3 being Real such that
A3: ( x = - r3 & r3 in f .: A ) ;
consider x1 being set such that
A4: ( x1 in X & x1 in A & r3 = f . x1 ) by A3, FUNCT_2:115;
x = (- f) . x1 by A3, A4, VALUED_1:8;
hence x in (- f) .: A by A4, FUNCT_2:43; :: thesis: verum

end;

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