let A be non empty set ; :: thesis: CAlgebra A is ComplexAlgebra
for x, y, z being Element of (CAlgebra A)
for a, b being Complex holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (CAlgebra A)) = x & x is right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (CAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) ) by Th29;
hence CAlgebra A is ComplexAlgebra by Def9, ALGSTR_0:def 16, GROUP_1:def 4, GROUP_1:def 16, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, VECTSP_1:def 11, VECTSP_1:def 13; :: thesis: verum