let n be Nat; :: thesis: count_reps ({},n) = EmptyBag n
set s = count_reps ({},n);
set E = EmptyBag n;
A1: ( dom (count_reps ({},n)) = n & n = dom (EmptyBag n) ) by PARTFUN1:def 2;
for x being object st x in dom (count_reps ({},n)) holds
(count_reps ({},n)) . x = (EmptyBag n) . x

proof

let x be object ; :: thesis: ( x in dom (count_reps ({},n)) implies (count_reps ({},n)) . x = (EmptyBag n) . x )
assume A2: x in dom (count_reps ({},n)) ; :: thesis: (count_reps ({},n)) . x = (EmptyBag n) . x
x in Segm n by A2;
then reconsider i = x as Nat ;
thus (count_reps ({},n)) . x = card ({} " {(i + 1)}) by Def8, A2
.= (EmptyBag n) . x ; :: thesis: verum

end;

hence count_reps ({},n) = EmptyBag n by A1; :: thesis: verum