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 Th31;

A2: now

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

end;

A4: now

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

end;

now

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

now

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

A9: now

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

end;

now

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

end;

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

end;

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

end;

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