theorem Th63: :: EXCHSORT:63

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