1.1 --- a/src/HOL/Finite_Set.thy	Thu Jun 04 23:42:11 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Jun 05 09:54:26 2009 +0200
     1.3 @@ -2228,6 +2228,9 @@
     1.4  lemma card_image: "inj_on f A ==> card (f ` A) = card A"
     1.5  by(simp add:card_def setsum_reindex o_def del:setsum_constant)
     1.6  
     1.7 +lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
     1.8 +by(auto simp: card_image bij_betw_def)
     1.9 +
    1.10  lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
    1.11  by (simp add: card_seteq card_image)
    1.12