for p being XFinSequence
for x being object holds last (p ^ <%x%>) = x