let n be Nat; :: thesis: for k being non zero Real
for m being odd Integer holds (k to_power m) to_power n = k to_power (m * n)
let k be non zero Real; :: 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)
k to_power (m * n) = k #Z (m * n) by POWER:def 2
.= (k #Z m) #Z n by PREPOWER:45
.= (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