let a be Real; :: thesis: for k being Integer st k is odd holds
(- a) to_power k = - (a to_power k)
let k be Integer; :: thesis: ( k is odd implies (- a) to_power k = - (a to_power k) )
assume A1: k is odd ; :: thesis: (- a) to_power k = - (a to_power k)
then consider l being Integer such that
A2: k = (2 * l) + 1 by ABIAN:1;

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

suppose A3: a = 0 ; :: thesis: (- a) to_power k = - (a to_power k)

k <> 0 by A1;
then a to_power k = 0 by A3, Th42;
hence (- a) to_power k = - (a to_power k) by A3; :: thesis: verum

end;

suppose A4: a > 0 ; :: thesis: (- a) to_power k = - (a to_power k)

then A5: - a <> - 0 ;
a to_power k = (a to_power (2 * l)) * (a to_power 1) by A2, A4, Th27
.= (a to_power (2 * l)) * a
.= ((- a) to_power (2 * l)) * a by Th47
.= - (((- a) to_power (2 * l)) * (- a))
.= - (((- a) #Z (2 * l)) * (- a)) by Def2
.= - (((- a) #Z (2 * l)) * ((- a) #Z 1)) by PREPOWER:35
.= - ((- a) #Z k) by A2, A5, PREPOWER:44
.= - ((- a) to_power k) by Def2 ;
hence (- a) to_power k = - (a to_power k) ; :: thesis: verum

end;

suppose A6: a < 0 ; :: thesis: (- a) to_power k = - (a to_power k)

then - a > 0 by XREAL_1:58;
hence (- a) to_power k = ((- a) to_power (2 * l)) * ((- a) to_power 1) by A2, Th27
.= ((- a) to_power (2 * l)) * (- a)
.= (a to_power (2 * l)) * (- a) by Th47
.= - ((a to_power (2 * l)) * a)
.= - ((a #Z (2 * l)) * a) by Def2
.= - ((a #Z (2 * l)) * (a #Z 1)) by PREPOWER:35
.= - (a #Z k) by A2, A6, PREPOWER:44
.= - (a to_power k) by Def2 ;
:: thesis: verum

end;

end;