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 :: thesis: for x being object holds
( ( x in (- f) " A implies x in f " (-- A) ) & ( x in f " (-- A) implies x in (- f) " A ) )

let x be object ; :: thesis: ( ( x in (- f) " A implies x in f " (-- A) ) & ( x in f " (-- A) implies x in (- f) " A ) )
reconsider xx = x as set by TARSKI:1;

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

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

end;

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

end;

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