theorem Th4: :: SIN_COS:4

for k being Nat
for seq being Complex_Sequence st 0 < k holds
(Shift seq) . k = seq . (k -' 1)