let k, m be Nat; :: thesis: for a being real number holds a to_power (k + m) = (a to_power k) * (a to_power m)
let a be real number ; :: thesis: a to_power (k + m) = (a to_power k) * (a to_power m)
thus a to_power (k + m) = a |^ (k + m) by POWER:46
.= (a |^ k) * (a |^ m) by NEWTON:13
.= (a to_power k) * (a |^ m) by POWER:46
.= (a to_power k) * (a to_power m) by POWER:46 ; :: thesis: verum