let a be real number ; :: thesis: for k being Integer st a <> 0 & k is even holds
(- a) to_power k = a to_power k
let k be Integer; :: thesis: ( a <> 0 & k is even implies (- a) to_power k = a to_power k )
assume A1: a <> 0 ; :: thesis: ( not k is even or (- a) to_power k = a to_power k )
given l being Integer such that A2: k = 2 * l ; :: according to ABIAN:def 1 :: thesis: (- a) to_power k = a to_power k
reconsider l1 = 2 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

thus a to_power k = (a to_power 2) to_power l by A2, A4, Th38
.= (a ^2 ) to_power l by Th53
.= ((- a) ^2 ) to_power l
.= ((- a) to_power 2) to_power l by Th53
.= ((- a) #Z l1) to_power l by Def2
.= ((- a) #Z l1) #Z l by Def2
.= (- a) #Z (l1 * l) by PREPOWER:55
.= (- a) to_power k by A2, Def2 ; :: thesis: verum

end;

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

A6: - a > 0 by A5, XREAL_1:60;
thus (- a) to_power k = ((- a) to_power 2) to_power l by A2, A6, Th38
.= ((- a) ^2 ) to_power l by Th53
.= (a ^2 ) to_power l
.= (a to_power 2) to_power l by Th53
.= (a #Z l1) to_power l by Def2
.= (a #Z l1) #Z l by Def2
.= a #Z (l1 * l) by PREPOWER:55
.= a to_power k by A2, Def2 ; :: thesis: verum

end;

end;

end;

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