src/HOL/Cardinals/Cardinal_Arithmetic.thy

 by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[OF assms]])
 
 lemma czero_cexp: "Cnotzero r \<Longrightarrow> czero ^c r =o czero"
   by (drule Cnotzero_imp_not_empty) (simp add: cexp_def czero_def card_of_empty_ordIso)
 
-lemma Func_singleton: 
+lemma Func_singleton:
 fixes x :: 'b and A :: "'a set"
 shows "|Func A {x}| =o |{x}|"
 proof (rule ordIso_symmetric)
   def f \<equiv> "\<lambda>y a. if y = x \<and> a \<in> A then x else undefined"
   have "Func A {x} \<subseteq> f ` {x}" unfolding f_def Func_def by (force simp: fun_eq_iff)