:: deftheorem defines ComplexFuncZero CFUNCDOM:def 4 :
for A being non empty set holds ComplexFuncZero A = A --> 0;