:: deftheorem defines prime-factorization-like INT_7:def 1 :
for p being bag of SetPrimes holds
( p is prime-factorization-like iff for x being Prime st x in support p holds
ex n being Nat st
( 0 < n & p . x = x |^ n ) );