let A be array; :: thesis: for B being permutation of A holds
( dom B = dom A & rng B = rng A )
let B be permutation of A; :: thesis: ( dom B = dom A & rng B = rng A )
consider f being Permutation of (dom A) such that
A1: B = A * f by Def9;
( dom A <> {} implies dom A <> {} ) ;
then ( rng f = dom A & dom f = dom A ) by FUNCT_2:def 1, FUNCT_2:def 3;
hence ( dom B = dom A & rng B = rng A ) by A1, RELAT_1:27, RELAT_1:28; :: thesis: verum