for p being Prime
for n being non zero Nat holds p |-count (Radical n) <= p |-count n by Th55, NAT_3:30;