theorem Th44: :: VALUED_1:45

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