for X being Complex_Banach_Algebra
for k being Nat
for seq being sequence of X st 0 < k holds
(Shift seq) . k = seq . (k -' 1) by LOPBAN_4:15;