Let f, X, Y and x be given.
Assume Htot: total_function_on f X Y.
Assume HxX: x ∈ X.
We will prove (x,apply_fun f x) ∈ f.
We prove the intermediate claim Hex: ∃y : set, y ∈ Y ∧ (x,y) ∈ f.
An exact proof term for the current goal is (total_function_on_totality f X Y Htot x HxX).
Set y0 to be the term Eps_i (λy : set ⇒ y ∈ Y ∧ (x,y) ∈ f).
We prove the intermediate claim Hy0: y0 ∈ Y ∧ (x,y0) ∈ f.
An exact proof term for the current goal is (Eps_i_ex (λy : set ⇒ y ∈ Y ∧ (x,y) ∈ f) Hex).
We prove the intermediate claim Hxy0: (x,y0) ∈ f.
An exact proof term for the current goal is (andER (y0 ∈ Y) ((x,y0) ∈ f) Hy0).
An exact proof term for the current goal is (Eps_i_ax (λy : set ⇒ (x,y) ∈ f) y0 Hxy0).
∎