Let f, X, Y and Z be given.

Assume Hfun: function_on f X Y.

Assume HYZ: Y ⊆ Z.

Let x be given.

Assume HxX: x ∈ X.

We will prove apply_fun f x ∈ Z.

An exact proof term for the current goal is (HYZ (apply_fun f x) (Hfun x HxX)).

∎