let A be non empty set ; :: thesis: for f being Element of Funcs (A,COMPLEX)
for a, b being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f]
let f be Element of Funcs (A,COMPLEX); :: thesis: for a, b being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f]
let a, b be Complex; :: thesis: (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f]

now

let x be Element of A; :: thesis: ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f]))) . x = ((ComplexFuncExtMult A) . [(a + b),f]) . x
thus ((ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f]))) . x = (((ComplexFuncExtMult A) . [a,f]) . x) + (((ComplexFuncExtMult A) . [b,f]) . x) by Th1
.= (a * (f . x)) + (((ComplexFuncExtMult A) . [b,f]) . x) by Th6
.= (a * (f . x)) + (b * (f . x)) by Th6
.= (a + b) * (f . x)
.= ((ComplexFuncExtMult A) . [(a + b),f]) . x by Th6 ; :: thesis: verum

end;

hence (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f] by FUNCT_2:63; :: thesis: verum