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

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