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

now

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

end;

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