theorem Th31: :: EXCHSORT:31

for x, y being set
for f being Function st x in dom f & y in dom f holds
(Swap (f,x,y)) . y = f . x