theorem :: COMPLEX3:91

for a, m, n being positive Real holds (a to_power n) + (a to_power m) = (a to_power (min (n,m))) * (1 + (a to_power |.(m - n).|))