theorem Th34: :: EXCHSORT:34

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