theorem Th37: :: AFINSQ_1:40

for p being XFinSequence st p <> {} holds
ex q being XFinSequence ex x being object st p = q ^ <%x%>