theorem Th32: :: EXCHSORT:32

for x, y, X being set
for f being array of X st x in dom f & y in dom f holds
(Swap (f,x,y)) /. y = f /. x