Let A, Y and g be given.

Assume Hg: ∀a : set, a ∈ A → g a ∈ Y.

We prove the intermediate claim Htot: total_function_on (graph A g) A Y.

An exact proof term for the current goal is (total_function_on_graph A Y g Hg).

We prove the intermediate claim Hfun: function_on (graph A g) A Y.

An exact proof term for the current goal is (andEL (function_on (graph A g) A Y) (∀a : set, a ∈ A → ∃y : set, y ∈ Y ∧ (a,y) ∈ graph A g) Htot).

We prove the intermediate claim Hsub: graph A g ⊆ setprod A Y.

An exact proof term for the current goal is (graph_subset_setprod A Y g Hg).

We prove the intermediate claim Hpow: graph A g ∈ 𝒫 (setprod A Y).

An exact proof term for the current goal is (PowerI (setprod A Y) (graph A g) Hsub).

An exact proof term for the current goal is (SepI (𝒫 (setprod A Y)) (λf0 : set ⇒ function_on f0 A Y) (graph A g) Hpow Hfun).

∎