theorem :: CFUNCDOM:26

for 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) )