for s, f being Function
for n being Nat holds Shift ((f * s),n) = f * (Shift (s,n))