add lemma additive.setsum

--- a/src/HOL/Real/RealVector.thy	Fri May 11 20:47:30 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Sat May 12 18:16:30 2007 +0200
@@ -32,6 +32,14 @@
 lemma (in additive) diff: "f (x - y) = f x - f y"
 by (simp add: diff_def add minus)
 
+lemma (in additive) setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
+apply (cases "finite A")
+apply (induct set: finite)
+apply (simp add: zero)
+apply (simp add: add)
+apply (simp add: zero)
+done
+
 
 subsection {* Real vector spaces *}