theorem Th44: :: HILB10_7:44

for f being finite Function
for p being Permutation of (dom f) holds
( f is with_evenly_repeated_values iff f * p is with_evenly_repeated_values )