theorem :: AFINSQ_1:92

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