[STATEMENT]
lemma ZFfunApp: 
  assumes "x |\<in>| A"
  shows   "(ZFfun A B f) |@| x = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFfun A B f |@| x = f x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ZFfun A B f |@| x = f x
[PROOF STEP]
have "(ZFfun A B f) |@| x = app (Lambda A f) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFfun A B f |@| x = Lambda A f \<acute> x
[PROOF STEP]
by (simp add: ZFfun_def ZFfunApp_def Snd)
[PROOF STATE]
proof (state)
this:
ZFfun A B f |@| x = Lambda A f \<acute> x

goal (1 subgoal):
 1. ZFfun A B f |@| x = f x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ZFfun A B f |@| x = Lambda A f \<acute> x

goal (1 subgoal):
 1. ZFfun A B f |@| x = f x
[PROOF STEP]
have "... = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Lambda A f \<acute> x = f x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x |\<in>| A

goal (1 subgoal):
 1. Lambda A f \<acute> x = f x
[PROOF STEP]
by (simp add: Lambda_app)
[PROOF STATE]
proof (state)
this:
Lambda A f \<acute> x = f x

goal (1 subgoal):
 1. ZFfun A B f |@| x = f x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ZFfun A B f |@| x = f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ZFfun A B f |@| x = f x

goal (1 subgoal):
 1. ZFfun A B f |@| x = f x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ZFfun A B f |@| x = f x

goal:
No subgoals!
[PROOF STEP]
qed