let A be non empty set ; :: thesis: for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f])) = ComplexFuncZero A
let f be Element of Funcs (A,COMPLEX); :: thesis: (ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f])) = ComplexFuncZero A
reconsider mj = - 1r as Element of COMPLEX by XCMPLX_0:def 2;

now :: thesis: for x being Element of A holds ((ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [mj,f]))) . x = (ComplexFuncZero A) . x

let x be Element of A; :: thesis: ((ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [mj,f]))) . x = (ComplexFuncZero A) . x
set y = f . x;
thus ((ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [mj,f]))) . x = (f . x) + (((ComplexFuncExtMult A) . [mj,f]) . x) by Th1
.= (f . x) + (mj * (f . x)) by Th4
.= (ComplexFuncZero A) . x by COMPLEX1:def 4, FUNCOP_1:7 ; :: thesis: verum

end;

hence (ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f])) = ComplexFuncZero A by FUNCT_2:63; :: thesis: verum