let a be Real; :: thesis: for n being Nat st a > 0 & n >= 1 holds
n -Root (1 / a) = 1 / (n -Root a)
let n be Nat; :: thesis: ( a > 0 & n >= 1 implies n -Root (1 / a) = 1 / (n -Root a) )
assume that
A1: a > 0 and
A2: n >= 1 and
A3: n -Root (1 / a) <> 1 / (n -Root a) ; :: thesis: contradiction
A4: n -Root a > 0 by A1, A2, Def2;
A5: (1 / (n -Root a)) |^ n = 1 / ((n -Root a) |^ n) by Th7
.= 1 / a by A1, A2, Lm2 ;
A6: n -Root (1 / a) > 0 by A1, A2, Def2;

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

suppose n -Root (1 / a) > 1 / (n -Root a) ; :: thesis: contradiction

hence contradiction by A2, A4, A5, Lm2; :: thesis: verum

end;

suppose n -Root (1 / a) < 1 / (n -Root a) ; :: thesis: contradiction

hence contradiction by A2, A5, A6, Lm2; :: thesis: verum

end;

end;