let F be finite set ; :: thesis: for E being Enumeration of F
for p being Permutation of (dom E) holds E * p is Enumeration of F
let E be Enumeration of F; :: thesis: for p being Permutation of (dom E) holds E * p is Enumeration of F
let p be Permutation of (dom E); :: thesis: E * p is Enumeration of F
reconsider Ep = E * p as FinSequence ;
( dom p = dom E & dom E = rng p ) by FUNCT_2:52, FUNCT_2:def 3;
then ( rng Ep = rng E & rng E = F ) by RELAT_1:28, RLAFFIN3:def 1;
hence E * p is Enumeration of F by RLAFFIN3:def 1; :: thesis: verum