theorem :: WSIERP_1:32

for a, b, f, g being Nat st f > 0 & g > 0 & f gcd g = 1 & a |^ f = b |^ g holds
ex e being Nat st
( a = e |^ g & b = e |^ f )