theorem Th15: :: LOPBAN_4:15

for k being Nat
for X being non empty ZeroStr
for seq being sequence of X st 0 < k holds
(Shift seq) . k = seq . (k -' 1)