consider A being non empty set ;
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;
then ( CAlgebra A is Abelian & CAlgebra A is add-associative & CAlgebra A is right_zeroed & CAlgebra A is right_complementable & CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is ComplexAlgebra-like & CAlgebra A is commutative & CAlgebra A is associative ) 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;
hence ex b₁ being non empty ComplexAlgebraStr st
( b₁ is strict & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is commutative & b₁ is associative & b₁ is right_unital & b₁ is right-distributive & b₁ is ComplexAlgebra-like ) ; :: thesis: verum