:: deftheorem defines last EXCHSORT:def 7 :
for A being array holds last A = A . (union (dom A));