src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Tue Oct 20 15:02:48 2009 +0100
+++ b/src/HOL/Fun.thy	Tue Oct 20 16:32:51 2009 +0100
@@ -78,6 +78,9 @@
 lemma image_compose: "(f o g) ` r = f`(g`r)"
 by (simp add: comp_def, blast)
 
+lemma vimage_compose: "(g \<circ> f) -` x = f -` (g -` x)"
+  by auto
+
 lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
 by (unfold comp_def, blast)