Let X, Y and f be given.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1 _ H2.
We will
prove (∀u ∈ X, f u ∈ Y) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H2.
∎