theorem Th46: :: FINSEQ_1:46

for p being FinSequence st p <> {} holds
ex q being FinSequence ex x being object st p = q ^ <*x*>