:: deftheorem Def6 defines with_evenly_repeated_values HILB10_7:def 6 :
for f being finite Function holds
( f is with_evenly_repeated_values iff for y being object holds card (f " {y}) is even );