theorem Th10: :: CFUNCDOM:10

for A being non empty set
for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . ((ComplexFuncZero A),f) = f