theorem Th14: :: FINSEQ_2:16

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