lemma powr_add_n:
  assumes "finite (X::real set)"
    and "X ≠ {}"
  shows "(∏y ∈ X. a powr y) = a powr (∑X)"
  using assms by (induct X rule: finite_ne_induct,auto)(simp add: powr_add)