Let A, Y and g be given.

Assume Hg: ∀a : set, a ∈ A → g a ∈ Y.

Let p be given.

Assume Hp: p ∈ graph A g.

We will prove p ∈ setprod A Y.

Apply (ReplE_impred A (λa0 : set ⇒ (a0,g a0)) p Hp (p ∈ setprod A Y)) to the current goal.

Let a be given.

Assume Ha: a ∈ A.

Assume Heq: p = (a,g a).

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma A Y a (g a) Ha (Hg a Ha)).

∎