theorem Th36: :: HILB10_7:36

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)*>