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