:: deftheorem defines ComplexFuncUnit CFUNCDOM:def 5 :
for A being non empty set holds ComplexFuncUnit A = A --> 1r;