Let U be given.

Assume HUT: TransSet U.

Assume HU: ZF_closed U.

Apply ZF_closed_E U HU to the current goal.

Assume HUU HUP HUR.

Let X be given.

Assume HX: X ∈ U.

Let Y be given.

Assume HY: ∀x ∈ X, Y x ∈ U.

We will prove (⋃_{x ∈ X}{setsum x y|y ∈ Y x}) ∈ U.

We prove the intermediate claim L1: famunion_closed U.

Apply Union_Repl_famunion_closed to the current goal.

An exact proof term for the current goal is HUU.

An exact proof term for the current goal is HUR.

Apply L1 X HX (λx ⇒ {setsum x y|y ∈ Y x}) to the current goal.

Let x be given.

Assume Hx: x ∈ X.

We will prove {setsum x y|y ∈ Y x} ∈ U.

Apply HUR (Y x) (HY x Hx) (λy ⇒ setsum x y) to the current goal.

Let y be given.

Assume Hy: y ∈ Y x.

We will prove setsum x y ∈ U.

Apply ZF_setsum_closed U HUT HU to the current goal.

We will prove x ∈ U.

An exact proof term for the current goal is HUT X HX x Hx.

We will prove y ∈ U.

An exact proof term for the current goal is HUT (Y x) (HY x Hx) y Hy.

∎