let a be real number ; :: thesis: for n being Element of NAT st ex m being Element of NAT st n = (2 * m) + 1 holds
n -root a = - (n -root (- a))
let n be Element of NAT ; :: thesis: ( ex m being Element of NAT st n = (2 * m) + 1 implies n -root a = - (n -root (- a)) )
assume A1: ex m being Element of NAT st n = (2 * m) + 1 ; :: thesis: n -root a = - (n -root (- a))
then consider m being Element of NAT such that
A2: n = (2 * m) + 1 ;
A3: n >= 0 + 1 by A2, XREAL_1:8;

now

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

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

then A5: - a >= 0 ;
thus n -root a = - (n -Root (- a)) by A1, A4, Def1
.= - (n -root (- a)) by A3, A5, Def1 ; :: thesis: verum

end;

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

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

end;

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

then - a < - 0 by XREAL_1:26;
hence - (n -root (- a)) = - (- (n -Root (- (- a)))) by A1, Def1
.= n -root a by A3, A7, Def1 ;
:: thesis: verum

end;

end;

end;

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