theorem Th16: :: CFUNCDOM:16

for A being non empty set
for f, g being Element of Funcs (A,COMPLEX)
for a being Complex holds (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]