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