let a be Real; :: thesis: for k being Integer st k is even holds
(- a) to_power k = a to_power k
let k be Integer; :: thesis: ( k is even implies (- a) to_power k = a to_power k )
given l being Integer such that A1: k = 2 * l ; :: according to INT_1:def 3,ABIAN:def 1 :: thesis: (- a) to_power k = a to_power k

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

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

hence (- a) to_power k = a to_power k ; :: thesis: verum

end;

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

hence a to_power k = (a to_power 2) to_power l by A1, Th33
.= (a ^2) to_power l by Th46
.= ((- a) ^2) to_power l
.= ((- a) to_power 2) to_power l by Th46
.= ((- a) #Z 2) to_power l by Def2
.= ((- a) #Z 2) #Z l by Def2
.= (- a) #Z (2 * l) by PREPOWER:45
.= (- a) to_power k by A1, Def2 ;
:: thesis: verum

end;

suppose 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) to_power l by A1, Th33
.= ((- a) ^2) to_power l by Th46
.= (a ^2) to_power l
.= (a to_power 2) to_power l by Th46
.= (a #Z 2) to_power l by Def2
.= (a #Z 2) #Z l by Def2
.= a #Z (2 * l) by PREPOWER:45
.= a to_power k by A1, Def2 ;
:: thesis: verum

end;

end;