[STATEMENT]
lemma Fun_incl:
    assumes "incl f"
    shows "Fun f = (\<lambda>x \<in> set (dom f). x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fun f = (\<lambda>x\<in>local.set (local.dom f). x)
[PROOF STEP]
using assms incl_def
[PROOF STATE]
proof (prove)
using this:
incl f
incl ?f = (arr ?f \<and> local.set (local.dom ?f) \<subseteq> local.set (cod ?f) \<and> ?f = mkArr (local.set (local.dom ?f)) (local.set (cod ?f)) (\<lambda>x. x))

goal (1 subgoal):
 1. Fun f = (\<lambda>x\<in>local.set (local.dom f). x)
[PROOF STEP]
by (metis Fun_mkArr)