:: deftheorem Def1 defines Shift VSDIFF_1:def 3 :
for F, G being Field
for V being VectSp of F
for W being VectSp of G
for f being PartFunc of V,W
for h being Element of V
for b₇ being PartFunc of V,W holds
( b₇ = Shift (f,h) iff ( dom b₇ = (- h) ++ (dom f) & ( for x being Element of V st x in (- h) ++ (dom f) holds
b₇ . x = f . (x + h) ) ) );