let A be array; :: thesis: for B being permutation of A holds B in Funcs ((dom A),(rng A))
let B be permutation of A; :: thesis: B in Funcs ((dom A),(rng A))
( dom B = dom A & rng B = rng A ) by ThDom;
hence B in Funcs ((dom A),(rng A)) by FUNCT_2:def 2; :: thesis: verum