English
Every variable occurring in bind₁ f φ comes from some variable i occurring in φ and from a variable appearing in f(i).
Русский
Любая переменная, встречающаяся в bind₁ f φ, берется из некоторой переменной i, встречающейся в φ, и из переменных, встречающихся в f(i).
LaTeX
$$$$ \forall j \in (\mathrm{bind}_1\, f\, \varphi).\mathrm{vars}, \; \exists i \in \mathrm{var}(\varphi),\; j \in (f(i)).\mathrm{vars} $$$$
Lean4
theorem mem_vars_bind₁ (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) {j : τ} (h : j ∈ (bind₁ f φ).vars) :
∃ i : σ, i ∈ φ.vars ∧ j ∈ (f i).vars := by
classical simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne] using vars_bind₁ f φ h