theorem Th29: :: EXCHSORT:29

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