for a, b being non zero Nat st ( for p being Element of NAT st p is prime holds
p |-count a = p |-count b ) holds
a = b