theorem Th17: :: FINSEQ_2:19

for A being set
for p being FinSequence of A st len p <> 0 holds
ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*>