theorem Th55: :: POLYNOM9:55

for i, n being Nat
for f being FinSequence holds count_reps ((f ^ <*(i + 1)*>),n) = (count_reps (f,n)) + ((EmptyBag n) +* (i,1))