1. R : Rng
2. Comm(|R|;*)
⊢ IsMonoid(|R|;*;1) ∧ BiLinear(|R|;+R;*) ∧ (∀a:|R|. Dist1op2opLR(|R|;* a;*))
{ D 1 }
1. R : RngSig
2. IsRing(|R|;+R;0;-R;*;1)
3. Comm(|R|;*)