let f be finite Function; :: thesis: for p being Permutation of (dom f) holds
( f is with_evenly_repeated_values iff f * p is with_evenly_repeated_values )
let p be Permutation of (dom f); :: thesis: ( f is with_evenly_repeated_values iff f * p is with_evenly_repeated_values )
set fp = f * p;
A1: ( dom p = dom f & dom f = rng p ) by FUNCT_2:52, FUNCT_2:def 3;
then A2: dom (f * p) = dom f by RELAT_1:27;
thus ( f is with_evenly_repeated_values implies f * p is with_evenly_repeated_values ) :: thesis: ( f * p is with_evenly_repeated_values implies f is with_evenly_repeated_values )

proof

assume A3: f is with_evenly_repeated_values ; :: thesis: f * p is with_evenly_repeated_values
let y be object ; :: according to HILB10_7:def 6 :: thesis: card ((f * p) " {y}) is even
card ((f * p) " {y}) = card (f " {y}) by A2, A1, CLASSES1:77, CLASSES1:78;
hence card ((f * p) " {y}) is even by A3; :: thesis: verum

end;

assume A4: f * p is with_evenly_repeated_values ; :: thesis: f is with_evenly_repeated_values
let y be object ; :: according to HILB10_7:def 6 :: thesis: card (f " {y}) is even
card ((f * p) " {y}) = card (f " {y}) by A2, A1, CLASSES1:77, CLASSES1:78;
hence card (f " {y}) is even by A4; :: thesis: verum