diff -r 75d14ac0547e -r 5827b91ef30e src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Sun Oct 03 21:29:34 2021 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Mon Oct 04 12:32:50 2021 +0100
@@ -110,6 +110,25 @@
   using to_nat_on_infinite[of S, unfolded bij_betw_def]
   by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
 
+text \<open>
+  The sum/product over the enumeration of a finite set equals simply the sum/product over the set
+\<close>
+context comm_monoid_set
+begin
+
+lemma card_from_nat_into:
+  "F (\<lambda>i. h (from_nat_into A i)) {..<card A} = F h A"
+proof (cases "finite A")
+  case True
+  have "F (\<lambda>i. h (from_nat_into A i)) {..<card A} = F h (from_nat_into A ` {..<card A})"
+    by (metis True bij_betw_def bij_betw_from_nat_into_finite reindex_cong)
+  also have "... = F h A"
+    by (metis True bij_betw_def bij_betw_from_nat_into_finite)
+  finally show ?thesis .
+qed auto
+
+end
+
 lemma countable_as_injective_image:
   assumes "countable A" "infinite A"
   obtains f :: "nat \<Rightarrow> 'a" where "A = range f" "inj f"