# HG changeset patch
# User nipkow
# Date 1244188487 -7200
# Node ID 4b56acf24a1a64fbac2ad1b2aaa50b4992c27194
# Parent  d0ffa8fad5bbbffd6bac43b50ffaadce83dc829d# Parent  9606881217389befc85ed998cd72634d05bc92f7
merged

diff -r d0ffa8fad5bb -r 4b56acf24a1a src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jun 05 00:29:29 2009 -0700
+++ b/src/HOL/Finite_Set.thy	Fri Jun 05 09:54:47 2009 +0200
@@ -2228,6 +2228,9 @@
 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
 
+lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
+by(auto simp: card_image bij_betw_def)
+
 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
 by (simp add: card_seteq card_image)