src/HOL/Set.thy

--- a/src/HOL/Set.thy	Sun Apr 17 22:38:50 2016 +0200
+++ b/src/HOL/Set.thy	Mon Apr 18 14:30:32 2016 +0100
@@ -1001,6 +1001,9 @@
   shows "\<exists>x\<in>A. P (f x)"
   using assms by auto
 
+lemma image_add_0 [simp]: "op+ (0::'a::comm_monoid_add) ` S = S"
+  by auto
+
 
 text \<open>
   \medskip Range of a function -- just a translation for image!