theorem Th55: :: VALUED_1:56

for i being Nat
for q being FinSubsequence holds dom (Seq q) = dom (Seq (Shift (q,i)))