theorem :: EXCHSORT:44

for x, y being set
for A, B being array st x in dom A & y in dom A & A is permutation of B holds
( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) )