{R : Type u} →
  {A : Type u_4} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] → [FaithfulSMul R A] → (I J : (Submodule R A)ˣ) → TensorProduct R ↥↑I ↥↑J ≃ₗ[R] ↥↑(I * J)