theorem Th23: :: HILB10_7:23

for x, y being object
for f, g being Function holds (Swap (f,x,y)) * g = Swap ((f * g),x,y)