theorem DivisorsMulti: :: NUMBER12:48

for a, b being Nat holds PrimeDivisors (a * b) = (PrimeDivisors a) \/ (PrimeDivisors b)