let n be natural number ; :: thesis: for a being real number st n is even & a <> 0 holds
(- a) to_power n = a to_power n
let a be real number ; :: thesis: ( n is even & a <> 0 implies (- a) to_power n = a to_power n )
assume ( n is even & a <> 0 ) ; :: thesis: (- a) to_power n = a to_power n
then ( a <> 0 & ex l being Integer st n = 2 * l ) by ABIAN:def 1;
hence (- a) to_power n = a to_power n by POWER:54; :: thesis: verum