theorem Th53: :: FINSEQ_3:55

for p, q being FinSequence
for k being Nat st len p = k + 1 & q = p | (Seg k) holds
p = q ^ <*(p . (k + 1))*>