theorem Th60: :: POLYNOM9:60

for n being Nat
for x being object
for f being finite Function st f is with_evenly_repeated_values holds
(count_reps (f,n)) . x is even