theorem :: FINSEQ_2:18

for i being natural Number
for p being FinSequence st len p = i + 1 holds
ex q being FinSequence ex a being object st p = q ^ <*a*> by CARD_1:27, FINSEQ_1:46;