theorem Th37: :: EXCHSORT:37
for A being array
for B being permutation of A holds
( dom B = dom A & rng B = rng A )