theorem :: HILB10_7:38

for x, y, z being object
for f being Function st z in dom f holds
swap ({(f . z)},x,y) = {((Swap (f,x,y)) . z)}