theorem :: AFINSQ_2:83

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