∀ {m : Type u_1} {n : Type u_2} (S : Type u_4) {A : Type u_3} [inst : Semiring S] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module S A] [SMulCommClass S A A] (x : m → A) (x_1 : S) (x_2 : n → A),
  Matrix.vecMulVec x (x_1 • x_2) = x_1 • Matrix.vecMulVec x x_2