{R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        (s : NonUnitalSubsemiring R) → (t : NonUnitalSubsemiring S) → ↥(s.prod t) ≃+* ↥s × ↥t