Let f and x be given.

Assume Hex: ∃y : set, (x,y) ∈ f.

We will prove (x,apply_fun f x) ∈ f.

An exact proof term for the current goal is (Eps_i_ex (λy : set ⇒ (x,y) ∈ f) Hex).

∎