Two basic lemmas on bij_betw.

--- a/src/HOL/Fun.thy	Fri Jun 20 09:55:31 2014 +0200
+++ b/src/HOL/Fun.thy	Sat Jun 21 10:41:02 2014 +0200
@@ -295,6 +295,13 @@
 apply (drule_tac x = x in spec, blast)
 done
 
+lemma bij_betw_imageI:
+  "\<lbrakk> inj_on f A; f ` A = B \<rbrakk> \<Longrightarrow> bij_betw f A B"
+unfolding bij_betw_def by clarify
+
+lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> f ` A = B"
+  unfolding bij_betw_def by clarify
+
 lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
   unfolding bij_betw_def by auto