theorem Th57: :: VALUED_1:58

for i being Nat
for k being Element of NAT
for q being FinSubsequence st k in dom (Seq q) holds
(Seq (Shift (q,i))) . k = (Seq q) . k