let a be real number ; :: thesis: for n being Element of NAT st a > 0 & n >= 1 holds
n -Root (1 / a) = 1 / (n -Root a)
let n be Element of NAT ; :: thesis: ( a > 0 & n >= 1 implies n -Root (1 / a) = 1 / (n -Root a) )
assume that
A1: ( a > 0 & n >= 1 ) and
A2: n -Root (1 / a) <> 1 / (n -Root a) ; :: thesis: contradiction
A4: n -Root a > 0 by A1, Def3;
A5: (1 / (n -Root a)) |^ n = 1 / ((n -Root a) |^ n) by Th14
.= 1 / a by A1, Lm2 ;
(n -Root a) " > 0 by A4;
then A6: 1 / (n -Root a) > 0 ;
A7: n -Root (1 / a) > 0 by A1, Def3;

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

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

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

end;

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

hence contradiction by A1, A5, A7, Lm2; :: thesis: verum

end;

end;