theorem DivSquare: :: NUMBER12:55

for a being Nat holds PrimeDivisors (a * a) = PrimeDivisors a