:: deftheorem Def9 defines permutation EXCHSORT:def 9 :
for A, b₂ being array holds
( b₂ is permutation of A iff ex f being Permutation of (dom A) st b₂ = A * f );