:: deftheorem Def7 defines with_evenly_repeated_values-member HILB10_7:def 7 :
for F being set holds
( F is with_evenly_repeated_values-member iff for y being object st y in F holds
y is finite with_evenly_repeated_values Function );