∀ (R : Type u_3) (S : Type u_4) (A : Type u_1) (B : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra S A]
  [inst_7 : Algebra S B] [inst_8 : SMulCommClass R S A] [inst_9 : TensorProduct.CompatibleSMul R S A B]
  (x x_1 : TensorProduct S A B),
  (∀ (y : TensorProduct S A B),
      (TensorProduct.mapOfCompatibleSMul R S A B) (x * y) =
        (TensorProduct.mapOfCompatibleSMul R S A B) x * (TensorProduct.mapOfCompatibleSMul R S A B) y) →
    (∀ (y : TensorProduct S A B),
        (TensorProduct.mapOfCompatibleSMul R S A B) (x_1 * y) =
          (TensorProduct.mapOfCompatibleSMul R S A B) x_1 * (TensorProduct.mapOfCompatibleSMul R S A B) y) →
      ∀ (x_2 : TensorProduct S A B),
        (TensorProduct.mapOfCompatibleSMul R S A B) ((x + x_1) * x_2) =
          (TensorProduct.mapOfCompatibleSMul R S A B) (x + x_1) * (TensorProduct.mapOfCompatibleSMul R S A B) x_2