theorem :: CFUNCDOM:29

for A being non empty set holds 1. (CAlgebra A) = ComplexFuncUnit A ;