Let f, X, Y and Z be given.
Assume Htot: total_function_on f X Y.
Assume HYZ: Y ⊆ Z.
We will prove function_on f X Z ∧ ∀x : set, x ∈ X → ∃y : set, y ∈ Z ∧ (x,y) ∈ f.
Apply andI to the current goal.
An exact proof term for the current goal is (function_on_codomain f X Y Z (total_function_on_function_on f X Y Htot) HYZ).
Let x be given.
Assume HxX: x ∈ X.
Apply (total_function_on_totality f X Y 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.
Apply andI to the current goal.
An exact proof term for the current goal is (HYZ y (andEL (y ∈ Y) ((x,y) ∈ f) Hy)).
An exact proof term for the current goal is (andER (y ∈ Y) ((x,y) ∈ f) Hy).
∎