let n be Nat; :: thesis: ( n is odd implies n -root (- 1) = - 1 )
assume A1: n is odd ; :: thesis: n -root (- 1) = - 1
then A2: n >= 1 by ABIAN:12;
thus n -root (- 1) = - (n -Root (- (- 1))) by A1, Def1
.= - 1 by A2, PREPOWER:20 ; :: thesis: verum