set R = the domRing;
take the domRing ; :: thesis: ( the domRing is Abelian & the domRing is left_zeroed & the domRing is right_zeroed & the domRing is add-associative & the domRing is right_complementable & the domRing is well-unital & the domRing is associative & the domRing is commutative & the domRing is distributive & the domRing is domRing-like )
thus ( the domRing is Abelian & the domRing is left_zeroed & the domRing is right_zeroed & the domRing is add-associative & the domRing is right_complementable & the domRing is well-unital & the domRing is associative & the domRing is commutative & the domRing is distributive & the domRing is domRing-like ) ; :: thesis: verum