theorem :: VALUED_1:23

for I, J being Function
for n being Nat holds Shift ((I +* J),n) = (Shift (I,n)) +* (Shift (J,n))