theorem :: CFUNCDOM:25

for A being non empty set holds CRing A is commutative Ring