theorem Th8: :: FLANG_1:8

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