theorem :: EXCHSORT:36

for x, y being set
for A being array st x in dom A & y in dom A holds
Swap ((Swap (A,x,y)),x,y) = A