let a, b be non zero Nat; :: thesis: ( ( for p being Element of NAT st p is prime holds
p |-count a = p |-count b ) implies a = b )
assume A1: for p being Element of NAT st p is prime holds
p |-count a = p |-count b ; :: thesis: a = b
then for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ;
then consider c being Element of NAT such that
A2: b = a * c by Th20;
for p being Element of NAT st p is prime holds
p |-count b <= p |-count a by A1;
then consider d being Element of NAT such that
A3: a = b * d by Th20;
a = a * (c * d) by A2, A3;
then c = 1 by NAT_1:15, XCMPLX_1:7;
hence a = b by A2; :: thesis: verum