let n be Nat; :: thesis: for q being real number st q > 0 & n > 0 holds

ex r being real number st q = r |^ n

let q be real number ; :: thesis: ( q > 0 & n > 0 implies ex r being real number st q = r |^ n )

assume ( q > 0 & n > 0 ) ; :: thesis: ex r being real number st q = r |^ n

then ( q > 0 & n >= 1 ) by NAT_1:14;

then A2: q = (n -Root q) |^ n by PREPOWER:19;

n -Root q in REAL by XREAL_0:def 1;

hence ex r being real number st q = r |^ n by A2; :: thesis: verum

ex r being real number st q = r |^ n

let q be real number ; :: thesis: ( q > 0 & n > 0 implies ex r being real number st q = r |^ n )

assume ( q > 0 & n > 0 ) ; :: thesis: ex r being real number st q = r |^ n

then ( q > 0 & n >= 1 ) by NAT_1:14;

then A2: q = (n -Root q) |^ n by PREPOWER:19;

n -Root q in REAL by XREAL_0:def 1;

hence ex r being real number st q = r |^ n by A2; :: thesis: verum