∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] (S : NonUnitalSubalgebra R A) [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B]
  (S₁ : NonUnitalSubalgebra R B), ↑(S.prod S₁) = ↑S ×ˢ ↑S₁