let A be array; :: thesis: A is permutation of A
take id (dom A) ; :: according to EXCHSORT:def 9 :: thesis: A = A * (id (dom A))
thus A = A * (id (dom A)) by RELAT_1:51; :: thesis: verum