let n be odd Integer; :: thesis: for m being non empty real number holds (- m) to_power n = - (m to_power n)
let m be non empty real number ; :: thesis: (- m) to_power n = - (m to_power n)
( m <> 0 & ex l being Integer st n = (2 * l) + 1 ) by ABIAN:1;
hence (- m) to_power n = - (m to_power n) by POWER:55; :: thesis: verum