∀ (R : Type u_10) {R₁ : Type u_1} {S₁ : Type u_2} {R₂ : Type u_6} {S₂ : Type u_7} {M₁ : Type u_3} {M₂ : Type u_5}
  {N₂ : Type u_4} {n : Type u_8} {m : Type u_9} [inst : CommSemiring R] [inst_1 : Semiring R₁] [inst_2 : Semiring S₁]
  [inst_3 : Semiring R₂] [inst_4 : Semiring S₂] [inst_5 : AddCommMonoid M₁] [inst_6 : Module R₁ M₁]
  [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] [inst_9 : AddCommMonoid N₂] [inst_10 : Module R N₂]
  [inst_11 : Module S₁ N₂] [inst_12 : Module S₂ N₂] [inst_13 : SMulCommClass S₁ R N₂] [inst_14 : SMulCommClass S₂ R N₂]
  [inst_15 : SMulCommClass S₂ S₁ N₂] {σ₁ : R₁ →+* S₁} {σ₂ : R₂ →+* S₂} (b₁ : n → M₁) (b₂ : m → M₂) (_f : R)
  (_g : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂),
  (Matrix.of fun i j => ((_f • _g) (b₁ i)) (b₂ j)) = Matrix.of fun i j => ((_f • _g) (b₁ i)) (b₂ j)