English
Let R, S, T be commutative semirings. If f : R →+* MvPolynomial(σ, S) and g : S →+* MvPolynomial(σ, T) are ring homomorphisms, then the two-step substitution obtained by first applying f and then g coincides with the substitution obtained by composing f and g and applying bind₂ once. In symbols, (bind₂ g) ∘ (bind₂ f) = bind₂(((bind₂ g) ∘ f)).
Русский
Пусть R, S, T — коммутативные полукольца. Пусть f : R →+* MvPolynomial(σ, S) и g : S →+* MvPolynomial(σ, T) — гомоморфизмы колец. Тогда последовательная подстановка, выполняемая сначала через f, затем через g, совпадает с подстановкой, полученной одной операцией bind₂ через композицию f и g. То есть (bind₂ g) ∘ (bind₂ f) = bind₂(((bind₂ g) ∘ f)).
LaTeX
$$$$ (\mathrm{bind}_2\, g) \circ (\mathrm{bind}_2\, f) = \mathrm{bind}_2\,((\mathrm{bind}_2\, g) \circ f) $$$$
Lean4
theorem bind₂_comp_bind₂ (f : R →+* MvPolynomial σ S) (g : S →+* MvPolynomial σ T) :
(bind₂ g).comp (bind₂ f) = bind₂ ((bind₂ g).comp f) := by ext : 2 <;> simp
