:: deftheorem Def12 defines Shift VALUED_1:def 12 :
for p being Function
for k being Nat
for b₃ being Function holds
( b₃ = Shift (p,k) iff ( dom b₃ = { (m + k) where m is Nat : m in dom p } & ( for m being Nat st m in dom p holds
b₃ . (m + k) = p . m ) ) );