have : ⟪i, f x⟫ ∈ seqMap hf s := H.seqMap_spec hix
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
s : M
H : Seq s
i : M
a✝¹ : i < s
x : M
a✝ : x < s
hix : ⟪i, x⟫ ∈ s
⊢ ∃ y < seqMap hf s, y = f x ∧ ⟪i, y⟫ ∈ seqMap hf s
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
s : M
H : Seq s
i : M
a✝¹ : i < s
x : M
a✝ : x < s
hix : ⟪i, x⟫ ∈ s
this : ⟪i, f x⟫ ∈ seqMap hf s
⊢ ∃ y < seqMap hf s, y = f x ∧ ⟪i, y⟫ ∈ seqMap hf s