theorem Th64: :: EXCHSORT:64

for f being Function
for O being non empty connected Poset
for T being non empty array of O
for p, q, r being Element of dom T st r in p & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] )