[isabelle] A new theorem about lambda

The following theorem is also missing in Isabelle/ZF core and should be added there:
lemma lam_is_fun: "f = (lam x:d. b(x)) ==> f: d->range(f)"
proof -
  assume eq: "f = (lam x:d. b(x))"
  have dom: "domain(f) = d" using domain_lam by (auto simp add: eq)
  with eq have "function(f)" using function_lam by auto
  with eq have "relation(f)" using relation_lam by auto
  ultimately have "f: domain(f)->range(f)" by (rule function_imp_Pi)
  with dom show ?thesis by auto
(I put it into my file ZF_Addons.thy.)
I'd like to hear a critique.
Victor Porton - http://portonvictor.org

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.