theorem :: MODELC_2:80

for k, n being Nat
for S being non empty set
for seq being Element of Inf_seq S holds Shift ((Shift (seq,k)),n) = Shift (seq,(n + k)) by Lm29;