# HG changeset patch
# User nipkow
# Date 1244188466 -7200
# Node ID 9606881217389befc85ed998cd72634d05bc92f7
# Parent  4fa98c1df7ba7cbd4c47b74ca9276579a026fe34
new lemma

diff -r 4fa98c1df7ba -r 960688121738 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Jun 04 23:42:11 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Jun 05 09:54:26 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)