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

now :: thesis: for x being object holds
( ( x in (q3 + f) " A implies x in f " ((- q3) ++ A) ) & ( x in f " ((- q3) ++ A) implies x in (q3 + f) " A ) )

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

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

assume A1: x in (q3 + f) " A ; :: thesis: x in f " ((- q3) ++ A)
then ( (q3 + f) . x in A & (q3 + f) . x = q3 + (f . xx) ) by FUNCT_2:38, VALUED_1:2;
then (- q3) + (q3 + (f . xx)) in { ((- q3) + p3) where p3 is Real : p3 in A } ;
then (- q3) + (q3 + (f . xx)) in (- q3) ++ A by Lm5;
hence x in f " ((- q3) ++ A) by A1, FUNCT_2:38; :: thesis: verum

end;

assume A2: x in f " ((- q3) ++ A) ; :: thesis: x in (q3 + f) " A
then ( f . x in (- q3) ++ A & (q3 + f) . x = q3 + (f . xx) ) by FUNCT_2:38, VALUED_1:2;
then (q3 + f) . x in { (q3 + p3) where p3 is Real : p3 in (- q3) ++ A } ;
then (q3 + f) . x in q3 ++ ((- q3) ++ A) by Lm5;
then (q3 + f) . x in (q3 + (- q3)) ++ A by MEMBER_1:147;
then (q3 + f) . x in A by MEMBER_1:146;
hence x in (q3 + f) " A by A2, FUNCT_2:38; :: thesis: verum

end;

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