theorem Th81: :: EXCHSORT:81

for x being set
for A being finite 0 -based array holds last (A ^ <%x%>) = x