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

per cases ( k > 0 or k < 0 ) ;

suppose k > 0 ; :: thesis: (k to_power m) to_power n = k to_power (m * n)

hence (k to_power m) to_power n = k to_power (m * n) by POWER:38; :: thesis: verum

end;

suppose k < 0 ; :: thesis: (k to_power m) to_power n = k to_power (m * n)

k to_power (m * n) = k #Z (m * n) by POWER:def 2
.= (k #Z m) #Z n by PREPOWER:55
.= (k to_power m) #Z n by POWER:def 2
.= (k to_power m) to_power n by POWER:def 2 ;
hence (k to_power m) to_power n = k to_power (m * n) ; :: thesis: verum

end;

end;