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