let x, y be Real; for d being Nat st x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d holds
x = y
let d be Nat; ( x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d implies x = y )
assume that
A1:
x >= 0
and
A2:
y >= 0
and
A3:
d > 0
and
A4:
x |^ d = y |^ d
; x = y
A5:
d >= 1
by A3, NAT_1:14;
then x =
d -Root (x |^ d)
by A1, PREPOWER:19
.=
y
by A2, A4, A5, PREPOWER:19
;
hence
x = y
; verum