let a, d be Nat; :: thesis: ( ex q being Rational st a = q |^ d implies ex b being Nat st a = b |^ d )
assume ex q being Rational st a = q |^ d ; :: thesis: ex b being Nat st a = b |^ d
then consider k being Integer such that
A1: a = k |^ d by Th24;

A2: now :: thesis: ( a = 0 implies ex b being Nat st a = b |^ d )

assume A3: a = 0 ; :: thesis: ex b being Nat st a = b |^ d
then d <> 0 by A1, NEWTON:4;
then a = 0 |^ d by A3, NAT_1:14, NEWTON:11;
hence ex b being Nat st a = b |^ d ; :: thesis: verum

end;

per cases ( d <> 0 or d = 0 ) ;

suppose d <> 0 ; :: thesis: ex b being Nat st a = b |^ d

now :: thesis: ( k is not Nat implies ex b being Nat st a = b |^ d )

consider e being Nat such that
A4: ( d = 2 * e or d = (2 * e) + 1 ) by Lm4;
consider c being Nat such that
A5: ( k = c or k = - c ) by INT_1:2;
assume A6: k is not Nat ; :: thesis: ex b being Nat st a = b |^ d

A7: now :: thesis: ( d = (2 * e) + 1 implies ex b being Nat st a = b |^ d )

assume d = (2 * e) + 1 ; :: thesis: ex b being Nat st a = b |^ d
then - (c |^ d) = a by A1, A6, A5, Th2;
hence ex b being Nat st a = b |^ d by A2; :: thesis: verum

end;

now :: thesis: ( d = 2 * e implies ex b being Nat st a = b |^ d )

assume d = 2 * e ; :: thesis: ex b being Nat st a = b |^ d
then a = c |^ d by A1, A5, Th2;
hence ex b being Nat st a = b |^ d ; :: thesis: verum

end;

hence ex b being Nat st a = b |^ d by A4, A7; :: thesis: verum

end;

hence ex b being Nat st a = b |^ d by A1; :: thesis: verum

end;

suppose A8: d = 0 ; :: thesis: ex b being Nat st a = b |^ d

then a = 1 by A1, NEWTON:4;
then a = 1 |^ 0 ;
hence ex b being Nat st a = b |^ d by A8; :: thesis: verum

end;

end;