theorem :: CFUNCDOM:28

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