:: deftheorem Def1 defines Shift DIFF_1:def 1 :
for f being PartFunc of REAL,REAL
for h being Real
for b₃ being PartFunc of REAL,REAL holds
( b₃ = Shift (f,h) iff ( dom b₃ = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds
b₃ . x = f . (x + h) ) ) );