:: deftheorem Def2 defines Shift DIFF_1:def 2 :
for f being Function of REAL,REAL
for h being Real
for b₃ being Function of REAL,REAL holds
( b₃ = Shift (f,h) iff for x being Real holds b₃ . x = f . (x + h) );