theorem :: WSIERP_1:35

for a, b, c, d being Nat st a gcd b = 1 & a * b = c |^ d holds
ex e, f being Nat st
( a = e |^ d & b = f |^ d )