∀ (R : Type u_4) (S : Type u_1) (T : Type u_5) (A : Type u_2) (B : Type u_3) [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring T] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : Algebra S B] [inst_9 : Algebra T A]
  [inst_10 : SMulCommClass R T A] [inst_11 : SMulCommClass S T A] [inst_12 : SMulCommClass R S A]
  [inst_13 : TensorProduct.CompatibleSMul R S A B] (x y : TensorProduct S A B),
  (TensorProduct.mapOfCompatibleSMul R S T A B) (x * y) =
    (TensorProduct.mapOfCompatibleSMul R S T A B) x * (TensorProduct.mapOfCompatibleSMul R S T A B) y