∀ (R : Type u_3) (S₁ : Type u_2) (S₂ : Type u_1) [inst : CommSemiring R] (x y : MvPolynomial (S₁ ⊕ S₂) R),
  (MvPolynomial.sumRingEquiv R S₁ S₂).toFun (x + y) =
    (MvPolynomial.sumRingEquiv R S₁ S₂).toFun x + (MvPolynomial.sumRingEquiv R S₁ S₂).toFun y