let n be Nat; :: thesis: for x being object
for f being finite Function st f is with_evenly_repeated_values holds
(count_reps (f,n)) . x is even
let x be object ; :: thesis: for f being finite Function st f is with_evenly_repeated_values holds
(count_reps (f,n)) . x is even
let f be finite Function; :: thesis: ( f is with_evenly_repeated_values implies (count_reps (f,n)) . x is even )
assume A1: f is with_evenly_repeated_values ; :: thesis: (count_reps (f,n)) . x is even
A2: dom (count_reps (f,n)) = n by PARTFUN1:def 2;

per cases ( x in n or not x in n ) ;

suppose A3: x in n ; :: thesis: (count_reps (f,n)) . x is even

then x in Segm n ;
then reconsider i = x as Nat ;
(count_reps (f,n)) . i = card (f " {(i + 1)}) by Def8, A3;
hence (count_reps (f,n)) . x is even by A1, HILB10_7:def 6; :: thesis: verum

end;

suppose not x in n ; :: thesis: (count_reps (f,n)) . x is even

hence (count_reps (f,n)) . x is even by A2, FUNCT_1:def 2; :: thesis: verum

end;

end;