theorem Th6: :: INT_7:6

for f being FinSequence of NAT
for b being bag of SetPrimes
for a being Prime st b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b