let A be non empty set ; :: thesis: CRing A is commutative Ring
for x, y, z being Element of (CRing A) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CRing A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CRing A)) = x & (1. (CRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) by Th24;
hence CRing A is commutative Ring by ALGSTR_0:def 16, GROUP_1:def 3, GROUP_1:def 12, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 6, VECTSP_1:def 7; :: thesis: verum