Let y be given.

Assume Hy: y ∈ image_of f (U ∪ V).

We will prove y ∈ (image_of f U) ∪ (image_of f V).

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

Let x be given.

Assume HxUV: x ∈ U ∪ V.

Assume Hyx: y = apply_fun f x.

Apply (binunionE U V x HxUV) to the current goal.

Assume HxU: x ∈ U.

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

Apply binunionI1 to the current goal.

An exact proof term for the current goal is (ReplI U (λx0 : set ⇒ apply_fun f x0) x HxU).

Assume HxV: x ∈ V.

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

Apply binunionI2 to the current goal.

An exact proof term for the current goal is (ReplI V (λx0 : set ⇒ apply_fun f x0) x HxV).

Let y be given.

Assume Hy: y ∈ (image_of f U) ∪ (image_of f V).

We will prove y ∈ image_of f (U ∪ V).

Apply (binunionE (image_of f U) (image_of f V) y Hy) to the current goal.

Assume HyU: y ∈ image_of f U.

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

Let x be given.

Assume HxU: x ∈ U.

Assume Hyx: y = apply_fun f x.

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

An exact proof term for the current goal is (ReplI (U ∪ V) (λx0 : set ⇒ apply_fun f x0) x (binunionI1 U V x HxU)).

Assume HyV: y ∈ image_of f V.

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

Let x be given.

Assume HxV: x ∈ V.

Assume Hyx: y = apply_fun f x.

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

An exact proof term for the current goal is (ReplI (U ∪ V) (λx0 : set ⇒ apply_fun f x0) x (binunionI2 U V x HxV)).