Let A, Y and g be given.
Assume Hg: ∀a : set, a ∈ A → g a ∈ Y.
We will prove total_function_on (graph A g) A Y.
We will prove function_on (graph A g) A Y ∧ ∀a : set, a ∈ A → ∃y : set, y ∈ Y ∧ (a,y) ∈ (graph A g).
Apply andI to the current goal.
We will prove function_on (graph A g) A Y.
Let a be given.
Assume Ha: a ∈ A.
rewrite the current goal using (apply_fun_graph A g a Ha) (from left to right).
An exact proof term for the current goal is (Hg a Ha).
Let a be given.
Assume Ha: a ∈ A.
We use (g a) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (Hg a Ha).
An exact proof term for the current goal is (ReplI A (λa0 : set ⇒ (a0,g a0)) a Ha).
∎