let A be non empty set ; :: thesis: 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))]
let f, g be Element of Funcs (A,COMPLEX); :: thesis: for a being Complex holds (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]
let a be Complex; :: thesis: (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]
reconsider a = a as Element of COMPLEX by XCMPLX_0:def 2;

now :: thesis: for x being Element of A holds ((ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g)) . x = ((ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]) . x

let x be Element of A; :: thesis: ((ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g)) . x = ((ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]) . x
thus ((ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g)) . x = (((ComplexFuncExtMult A) . [a,f]) . x) * (g . x) by Th2
.= (a * (f . x)) * (g . x) by Th4
.= a * ((f . x) * (g . x))
.= a * (((ComplexFuncMult A) . (f,g)) . x) by Th2
.= ((ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]) . x by Th4 ; :: thesis: verum

end;

hence (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))] by FUNCT_2:63; :: thesis: verum