theorem Th83: :: FINSEQ_5:83

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