src/ZF/Finite.thy

 lemma lam_FiniteFun: "A: Fin(X) ==> (\<lambda>x\<in>A. b(x)) \<in> A -||> {b(x). x:A}"
 by (blast intro: fun_FiniteFunI lam_funtype)
 
 lemma FiniteFun_Collect_iff:
      "f \<in> FiniteFun(A, {y:B. P(y)})
-      <-> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))"
+      \<longleftrightarrow> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))"
 apply auto
 apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD])
 apply (blast dest: Pair_mem_PiD FiniteFun_is_fun)
 apply (rule_tac A1="domain(f)" in
        subset_refl [THEN [2] FiniteFun_mono, THEN subsetD])