let x, y be real number ; :: thesis: for d being Nat st x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d holds
x = y
let d be Nat; :: thesis: ( x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d implies x = y )
assume A1: ( x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d ) ; :: thesis: x = y
then A2: d >= 1 by NAT_1:14;
then x = d -Root (x |^ d) by A1, PREPOWER:28
.= y by A1, A2, PREPOWER:28 ;
hence x = y ; :: thesis: verum