for a, d being Nat st ex q being Rational st a = q |^ d holds
ex b being Nat st a = b |^ d