theorem Th27: :: MEASUR12:27

for F being Function
for x, y being object st x in dom F & y in dom F holds
Swap (F,x,y) = F * (Swap ((id (dom F)),x,y))