let a, m, n be positive Real; :: thesis: (a to_power n) + (a to_power m) = (a to_power (min (n,m))) * (1 + (a to_power |.(m - n).|))

per cases ( n >= m or n < m ) ;

suppose B1: n >= m ; :: thesis: (a to_power n) + (a to_power m) = (a to_power (min (n,m))) * (1 + (a to_power |.(m - n).|))

then n - m >= m - m by XREAL_1:9;
then reconsider k = n - m as non negative Real ;
a to_power n = a to_power (m + k)
.= (a to_power m) * (a to_power k) by POWER:27 ;
then (a to_power n) + (a to_power m) = (a to_power m) * (1 + (a to_power |.(- (m - n)).|))
.= (a to_power m) * (1 + (a to_power |.(m - n).|)) by COMPLEX1:52 ;
hence (a to_power n) + (a to_power m) = (a to_power (min (n,m))) * (1 + (a to_power |.(m - n).|)) by B1, XXREAL_0:def 9; :: thesis: verum

end;

suppose B1: n < m ; :: thesis: (a to_power n) + (a to_power m) = (a to_power (min (n,m))) * (1 + (a to_power |.(m - n).|))

then n - n < m - n by XREAL_1:9;
then reconsider k = m - n as positive Real ;
a to_power m = a to_power (n + k)
.= (a to_power n) * (a to_power k) by POWER:27 ;
then (a to_power n) + (a to_power m) = (a to_power n) * (1 + (a to_power |.(m - n).|)) ;
hence (a to_power n) + (a to_power m) = (a to_power (min (n,m))) * (1 + (a to_power |.(m - n).|)) by B1, XXREAL_0:def 9; :: thesis: verum

end;

end;