src/HOL/Product_Type.thy

--- a/src/HOL/Product_Type.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Product_Type.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -1184,6 +1184,14 @@
   "snd ` (A \<times> B) = (if A = {} then {} else B)"
   by force
 
+lemma fst_image_Sigma:
+  "fst ` (Sigma A B) = {x \<in> A. B(x) \<noteq> {}}"
+  by force
+
+lemma snd_image_Sigma:
+  "snd ` (Sigma A B) = (\<Union> x \<in> A. B x)"
+  by force
+
 lemma vimage_fst:
   "fst -` A = A \<times> UNIV"
   by auto