let n be natural number ; :: thesis: for a being real number st not n is even & a <> 0 holds
(- a) to_power n = - (a to_power n)
let a be real number ; :: thesis: ( not n is even & a <> 0 implies (- a) to_power n = - (a to_power n) )
assume ( not 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) + 1 ) by ABIAN:1;
hence (- a) to_power n = - (a to_power n) by POWER:55; :: thesis: verum