let x be Real; :: thesis: for n being Nat st x >= 0 & n <> 0 holds
(n -root x) |^ n = x
let n be Nat; :: thesis: ( x >= 0 & n <> 0 implies (n -root x) |^ n = x )
assume that
A1: x >= 0 and
A2: n <> 0 ; :: thesis: (n -root x) |^ n = x
n >= 0 + 1 by A2, NAT_1:13;
hence (n -root x) |^ n = x by A1, POWER:4; :: thesis: verum