add lema about card and vimage

--- a/src/HOL/Finite_Set.thy	Wed Feb 11 14:12:30 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Feb 11 14:15:59 2015 +0100
@@ -1638,6 +1638,8 @@
 shows "finite A"
 using assms finite_imageD finite_subset by blast
 
+lemma card_vimage_inj: "\<lbrakk> inj f; A \<subseteq> range f \<rbrakk> \<Longrightarrow> card (f -` A) = card A"
+by(auto 4 3 simp add: subset_image_iff inj_vimage_image_eq intro: card_image[symmetric, OF subset_inj_on])
 
 subsubsection {* Pigeonhole Principles *}