let A, B be array; :: thesis: ( A is permutation of B implies B is permutation of A )
assume A1: A is permutation of B ; :: thesis: B is permutation of A
then A2: dom A = dom B by Th37;
consider f being Permutation of (dom B) such that
A3: A = B * f by A1, Def9;
reconsider g = f " as Permutation of (dom A) by A2;
take g ; :: according to EXCHSORT:def 9 :: thesis: B = A * g
thus B = B * (id (dom B)) by RELAT_1:52
.= B * (f * g) by FUNCT_2:61
.= A * g by A3, RELAT_1:36 ; :: thesis: verum