let a be real number ; :: thesis: for n being Nat st a > 0 & n >= 1 holds
( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
let n be Nat; :: thesis: ( a > 0 & n >= 1 implies ( (n -Root a) |^ n = a & n -Root (a |^ n) = a ) )
assume A1: ( a > 0 & n >= 1 ) ; :: thesis: ( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
hence (n -Root a) |^ n = a by Def3; :: thesis: n -Root (a |^ n) = a
assume A2: n -Root (a |^ n) <> a ; :: thesis: contradiction

per cases ( n -Root (a |^ n) > a or n -Root (a |^ n) < a ) by A2, XXREAL_0:1;

suppose A3: n -Root (a |^ n) > a ; :: thesis: contradiction

a |^ n > 0 by A1, Th13;
hence contradiction by A1, A3, Def3; :: thesis: verum

end;

suppose A4: n -Root (a |^ n) < a ; :: thesis: contradiction

a |^ n > 0 by A1, Th13;
hence contradiction by A1, A4, Def3; :: thesis: verum

end;

end;