let A, B, C be array; :: thesis: ( A is permutation of B & B is permutation of C implies A is permutation of C )
assume ZZ: ( A is permutation of B & B is permutation of C ) ; :: thesis: A is permutation of C
then Z0: dom C = dom B by ThDom;
consider f being Permutation of (dom B) such that
Z1: A = B * f by ZZ, PERM;
consider g being Permutation of (dom C) such that
Z3: B = C * g by ZZ, PERM;
reconsider h = g * f as Permutation of (dom C) by Z0;
take h ; :: according to EXCHSORT:def 9 :: thesis: A = C * h
thus A = C * h by Z1, Z3, RELAT_1:36; :: thesis: verum