theorem :: VALUED_1:21

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