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)
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