English
Let R, S, T be commutative semirings. If f and g are ring homomorphisms as above and φ ∈ MvPolynomial(σ, R), then applying bind₂ with f and then with g to φ equals applying bind₂ with the composed map to φ.
Русский
Пусть R, S, T — коммутативные полукольца. Если f и g являются гомоморфизмами колец, как выше, и φ ∈ MvPolynomial(σ, R), то применение bind₂ сначала к f, затем к g к φ совпадает с применением bind₂ к композиции к φ.
LaTeX
$$$$ (\mathrm{bind}_2\, g) \circ (\mathrm{bind}_2\, f) = \mathrm{bind}_2\big( (\mathrm{bind}_2\, g) \circ f \big) $$$$
Lean4
theorem bind₂_bind₂ (f : R →+* MvPolynomial σ S) (g : S →+* MvPolynomial σ T) (φ : MvPolynomial σ R) :
(bind₂ g) (bind₂ f φ) = bind₂ ((bind₂ g).comp f) φ :=
RingHom.congr_fun (bind₂_comp_bind₂ f g) φ
