theorem Th40: :: VALUED_1:41

for i being Nat
for q being FinSubsequence ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (Shift (q,i)) & ( for k being Element of NAT st k in dom q holds
ss . k = i + k ) & ss is one-to-one )