lemma
  fixes X :: "real set"
  assumes "finite X"
    and "X ≠ {}"
    and "∀x ∈ X. x ≥ 0"
    and "a ≥ 0"
  shows "(∏y ∈ X. a powr y) = a powr (∑X)"
  using assms
proof (induct X rule: finite_ne_induct)
  case (singleton y)
  then have "(∑X) = y"
    using assms sorry