let n be even 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
ex l being Integer st n = 2 * l by ABIAN:def 1;
hence (- m) to_power n = m to_power n by POWER:54; :: thesis: verum