We prove the intermediate claim L1: ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → {g x|x ∈ X ∖ {0}} = {h x|x ∈ X ∖ {0}}.

Let X, g and h be given.

Assume H1: ∀x ∈ X, g x = h x.

We will prove {g x|x ∈ X ∖ {0}} = {h x|x ∈ X ∖ {0}}.

Apply (ReplEq_ext (X ∖ {0}) g h) to the current goal.

Let x be given.

Assume H2: x ∈ X ∖ {0}.

We will prove g x = h x.

Apply H1 to the current goal.

We will prove x ∈ X.

An exact proof term for the current goal is (setminusE1 X {0} x H2).

An exact proof term for the current goal is (In_rec_i_eq (λX f ⇒ {f x|x ∈ X ∖ {0}}) L1).