let a, b be non negative Real; :: thesis: for n being positive Nat holds
( a |^ n = b |^ n iff a = b )
let n be positive Nat; :: thesis: ( a |^ n = b |^ n iff a = b )
( ( a > b implies a |^ n > b |^ n ) & ( a < b implies a |^ n < b |^ n ) ) by NEWTON02:40;
hence ( a |^ n = b |^ n iff a = b ) by XXREAL_0:1; :: thesis: verum