theorem Th42: :: FINSEQ_1:42

for p being FinSequence
for x being object holds (p ^ <*x*>) . ((len p) + 1) = x