Let Y, x, X, g and y be given.

Assume Hy.

Let x' be given.

Assume Hx'.

We will prove (1 + (x' + - x) * y) * g x' ∈ ⋃_{y ∈ Y}{(1 + (x' + - x) * y) * g x'|x' ∈ X}.

Apply famunionI Y (λy ⇒ {(1 + (x' + - x) * y) * g x'|x' ∈ X}) y ((1 + (x' + - x) * y) * g x') Hy to the current goal.

We will prove (1 + (x' + - x) * y) * g x' ∈ {(1 + (x' + - x) * y) * g x'|x' ∈ X}.

An exact proof term for the current goal is ReplI X (λx' ⇒ (1 + (x' + - x) * y) * g x') x' Hx'.

∎