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