theorem :: MEASURE6:70
for X being set
for A being Subset of REAL
for f being Function of X,REAL
for q3 being Real holds (q3 + f) " A = f " ((- q3) ++ A)