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