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:4;
then a = 0 |^ d by A3, NAT_1:14, NEWTON:11;
hence ex b being Nat st a = b |^ d ; :: thesis: verum

end;

A4: now

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

now

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

A8: now

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

end;

now

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

end;

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

end;

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

end;

now

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

end;

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