theorem :: NEWTON03:105

for n being Nat
for a being non trivial Nat
for b being non zero Integer holds a |-count ((a |^ n) * b) = n + (a |-count b)