let a be Real; :: 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 that
A1: a > 0 and
A2: n >= 1 ; :: thesis: ( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
thus (n -Root a) |^ n = a by A1, A2, Def2; :: thesis: n -Root (a |^ n) = a
assume A3: n -Root (a |^ n) <> a ; :: thesis: contradiction

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

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

a |^ n > 0 by A1, Th6;
hence contradiction by A1, A2, A4, Def2; :: thesis: verum

end;

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

a |^ n > 0 by A1, Th6;
hence contradiction by A1, A2, A5, Def2; :: thesis: verum

end;

end;