src/HOL/Library/Product_plus.thy

--- a/src/HOL/Library/Product_plus.thy	Thu Jul 01 08:13:20 2010 +0200
+++ b/src/HOL/Library/Product_plus.thy	Thu Jul 01 09:01:09 2010 +0200
@@ -118,4 +118,7 @@
 lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
 by (cases "finite A", induct set: finite, simp_all)
 
+lemma setsum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
+by (cases "finite A", induct set: finite) (simp_all add: zero_prod_def)
+
 end