theorem :: NEWTON03:43

for a, b, n being Nat
for p being prime Nat st a * b = p |^ n holds
ex k, l being Nat st
( a = p |^ k & b = p |^ l & k + l = n )