theorem Th8: :: FINSEQ_5:8

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