let m be non empty real number ; :: thesis: for n being Integer holds ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)
let n be Integer; :: thesis: ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)

per cases ( not n is even or n is even ) ;

suppose A1: not n is even ; :: thesis: ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)

then (- m) to_power n = - (m to_power n) by POWER:48
.= (- 1) * (m to_power n)
.= ((- 1) to_power n) * (m to_power n) by A1, Th3 ;
hence ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n) ; :: thesis: verum

end;

suppose A2: n is even ; :: thesis: ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)

then (- m) to_power n = 1 * (m to_power n) by POWER:47
.= ((- 1) to_power n) * (m to_power n) by A2, Th5 ;
hence ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n) ; :: thesis: verum

end;

end;