Let f, X, Y and A be given.

Assume Hfun: function_on f X Y.

Assume HA: A ⊆ X.

Let a be given.

Assume HaA: a ∈ A.

We will prove apply_fun f a ∈ Y.

We prove the intermediate claim HaX: a ∈ X.

An exact proof term for the current goal is (HA a HaA).

An exact proof term for the current goal is (Hfun a HaX).

∎