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