let a, b be Nat; :: thesis: ( ex q being Rational st a = q |^ b implies ex k being Integer st a = k |^ b )
given q being Rational such that A1: a = q |^ b ; :: thesis: ex k being Integer st a = k |^ b

now

A2: now

assume A3: b = 0 ; :: thesis: ex k being Integer st a = k |^ b
then a = 1 by A1, NEWTON:9;
then a = 1 |^ 0 by NEWTON:9;
hence ex k being Integer st a = k |^ b by A3; :: thesis: verum

end;

now

assume A4: b <> 0 ; :: thesis: ex k being Integer st a = k |^ b
set k = numerator q;
set d = denominator q;
A5: q = (numerator q) / (denominator q) by RAT_1:37;
denominator q <> 0 by RAT_1:def 3;
then A6: (denominator q) |^ b <> 0 by CARD_4:51;
a = ((numerator q) |^ b) / ((denominator q) |^ b) by A1, A5, PREPOWER:15;
then A7: a * ((denominator q) |^ b) = (numerator q) |^ b by A6, XCMPLX_1:88;
(numerator q) |^ b, denominator q are_relative_prime by Th15, Th29;
then A8: ((numerator q) |^ b) gcd (denominator q) = 1 by INT_2:def 4;
consider e being Nat such that
A9: e + 1 = b by A4, NAT_1:6;
(numerator q) |^ b = a * (((denominator q) |^ e) * (denominator q)) by A7, A9, NEWTON:11
.= (a * ((denominator q) |^ e)) * (denominator q) ;
then denominator q divides (numerator q) |^ b by INT_1:def 9;
then ( denominator q = 1 or denominator q = - 1 ) by A8, INT_2:17, INT_2:33;
hence ex k being Integer st a = k |^ b by A1, A5, INT_2:9; :: thesis: verum

end;

hence ex k being Integer st a = k |^ b by A2; :: thesis: verum

end;

hence ex k being Integer st a = k |^ b ; :: thesis: verum