theorem Th42: :: VALUED_1:43

for i being Nat
for p being FinSequence holds dom p = dom (Seq (Shift (p,i)))