theorem Th30: :: EXCHSORT:30

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)) /. x = f /. y