for p being FinSequence
for i being Nat st i + 1 <= len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>