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 A0: not n is even ; :: thesis: n -root a = - (n -root (- a))
then A1: ex m being Element of NAT st n = (2 * m) + 1 by ABIAN:9;
A2: n >= 1 by A0, Lm1;

A3: now

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

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

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

end;

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

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

end;

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

A7: - a < - 0 by A6, XREAL_1:26;
thus - (n -root (- a)) = - (- (n -Root (- (- a)))) by A1, A7, Def1
.= n -root a by A2, A6, Def1 ; :: thesis: verum

end;

end;

end;

thus n -root a = - (n -root (- a)) by A3; :: thesis: verum