let n be Element of NAT ; :: thesis: ( not n is even implies n -root (- 1) = - 1 )
assume A1: not n is even ; :: 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:29 ; :: thesis: verum