let a be real number ; :: thesis: for k being Integer st a <> 0 & not k is even holds
(- a) to_power k = - (a to_power k)
let k be Integer; :: thesis: ( a <> 0 & not k is even implies (- a) to_power k = - (a to_power k) )
assume A1: a <> 0 ; :: thesis: ( k is even or (- a) to_power k = - (a to_power k) )
assume not k is even ; :: thesis: (- a) to_power k = - (a to_power k)
then consider l being Integer such that
A2: k = (2 * l) + 1 by ABIAN:1;
reconsider l1 = 1 as Integer ;

A3: now

per cases ( a > 0 or a < 0 ) by A1;

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

A5: - a <> - 0 by A4;
A6: a to_power k = (a to_power (2 * l)) * (a to_power 1) by A2, A4, Th32
.= (a to_power (2 * l)) * a by Th30
.= ((- a) to_power (2 * l)) * a by A1, Th54
.= - (((- a) to_power (2 * l)) * (- a))
.= - (((- a) #Z (2 * l)) * (- a)) by Def2
.= - (((- a) #Z (2 * l)) * ((- a) #Z l1)) by PREPOWER:45
.= - ((- a) #Z k) by A2, A5, PREPOWER:54
.= - ((- a) to_power k) by Def2 ;
thus (- a) to_power k = - (a to_power k) by A6; :: thesis: verum

end;

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

A8: - a > 0 by A7, XREAL_1:60;
thus (- a) to_power k = ((- a) to_power (2 * l)) * ((- a) to_power 1) by A2, A8, Th32
.= ((- a) to_power (2 * l)) * (- a) by Th30
.= (a to_power (2 * l)) * (- a) by A1, Th54
.= - ((a to_power (2 * l)) * a)
.= - ((a #Z (2 * l)) * a) by Def2
.= - ((a #Z (2 * l)) * (a #Z l1)) by PREPOWER:45
.= - (a #Z k) by A2, A7, PREPOWER:54
.= - (a to_power k) by Def2 ; :: thesis: verum

end;

end;

end;

thus (- a) to_power k = - (a to_power k) by A3; :: thesis: verum