Let f, X, Y and U be given.

Assume Hfun: function_on f X Y.

Assume HUX: U ⊆ X.

Let y be given.

Assume Hy: y ∈ image_of f U.

We will prove y ∈ Y.

Apply (ReplE_impred U (λx : set ⇒ apply_fun f x) y Hy) to the current goal.

Let x be given.

Assume HxU: x ∈ U.

Assume Hyx: y = apply_fun f x.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HUX x HxU).

We prove the intermediate claim HfxY: apply_fun f x ∈ Y.

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

rewrite the current goal using Hyx (from left to right).

An exact proof term for the current goal is HfxY.

∎