theorem Th24: :: HILB10_7:24

for x, y being object
for X being set
for f being Function holds (Swap (f,x,y)) | X = Swap ((f | X),x,y)