let p, q be bag of SetPrimes ; :: thesis: ( p is prime-factorization-like & q is prime-factorization-like & Product p = Product q implies p = q )
assume that
A1: p is prime-factorization-like and
A2: q is prime-factorization-like and
A3: Product p = Product q ; :: thesis: p = q
reconsider n = Product p as Element of NAT ;
n <= 2 |^ n by NEWTON:86;
hence p = q by A1, A2, A3, Lm11; :: thesis: verum