for i being Nat
for p being FinSequence holds dom (Shift (p,i)) = { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) }