let k, m be Nat; :: thesis: for a being Real holds a to_power (k + m) = (a to_power k) * (a to_power m)
let a be Real; :: 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:41
.= (a |^ k) * (a |^ m) by NEWTON:8
.= (a to_power k) * (a |^ m) by POWER:41
.= (a to_power k) * (a to_power m) by POWER:41 ; :: thesis: verum