Let U be given.

Assume HU: Union_closed U.

Assume HR: Repl_closed U.

Let X be given.

Assume HX: X ∈ U.

Let F be given.

Assume HF: ∀x ∈ X, F x ∈ U.

We will prove famunion X F ∈ U.

We will prove ⋃ {F x|x ∈ X} ∈ U.

Apply HU to the current goal.

We will prove {F x|x ∈ X} ∈ U.

An exact proof term for the current goal is HR X HX F HF.

∎