let a be real number ; :: thesis: for n being Element of NAT st not n is even holds
n -root a = - (n -root (- a))
let n be Element of NAT ; :: thesis: ( not n is even implies n -root a = - (n -root (- a)) )
assume A1: not n is even ; :: thesis: n -root a = - (n -root (- a))
then A2: ex m being Element of NAT st n = (2 * m) + 1 by ABIAN:9;
A3: n >= 1 by A1, ABIAN:12;

now

per cases ( a < 0 or a = 0 or a > 0 ) ;

suppose A4: a < 0 ; :: thesis: n -root a = - (n -root (- a))

hence n -root a = - (n -Root (- a)) by A2, Def1
.= - (n -root (- a)) by A3, A4, Def1 ;
:: thesis: verum

end;

suppose A5: a = 0 ; :: thesis: n -root a = - (n -root (- a))

hence n -root a = 0 by A3, Th6
.= - (n -root (- a)) by A3, A5, Th6 ;
:: thesis: verum

end;

suppose A6: a > 0 ; :: thesis: - (n -root (- a)) = n -root a

then - a < - 0 by XREAL_1:24;
hence - (n -root (- a)) = - (- (n -Root (- (- a)))) by A2, Def1
.= n -root a by A3, A6, Def1 ;
:: thesis: verum

end;

end;

end;

hence n -root a = - (n -root (- a)) ; :: thesis: verum