Let X, Y and f be given.

Assume Htot: ∀x : set, x ∈ X → ∃y : set, y ∈ Y ∧ (x,y) ∈ f.

Assume Hrange: graph_range_subset f Y.

Let x be given.

Assume HxX: x ∈ X.

We will prove apply_fun f x ∈ Y.

We prove the intermediate claim Hex: ∃y : set, (x,y) ∈ f.

Apply (Htot x HxX) to the current goal.

Let y be given.

Assume Hy: y ∈ Y ∧ (x,y) ∈ f.

We use y to witness the existential quantifier.

An exact proof term for the current goal is (andER (y ∈ Y) ((x,y) ∈ f) Hy).

We prove the intermediate claim Hpair: (x,apply_fun f x) ∈ f.

An exact proof term for the current goal is (apply_fun_in_graph_of_ex f x Hex).

An exact proof term for the current goal is (Hrange x (apply_fun f x) Hpair).

∎