let X be non empty set ; :: thesis: for Y being ComplexLinearSpace
for f being Element of Funcs X,the carrier of Y holds (FuncAdd X,Y) . f,((FuncExtMult X,Y) . [(- 1r ),f]) = FuncZero X,Y
let Y be ComplexLinearSpace; :: thesis: for f being Element of Funcs X,the carrier of Y holds (FuncAdd X,Y) . f,((FuncExtMult X,Y) . [(- 1r ),f]) = FuncZero X,Y
let f be Element of Funcs X,the carrier of Y; :: thesis: (FuncAdd X,Y) . f,((FuncExtMult X,Y) . [(- 1r ),f]) = FuncZero X,Y

now

let x be Element of X; :: thesis: ((FuncAdd X,Y) . f,((FuncExtMult X,Y) . [(- 1r ),f])) . x = (FuncZero X,Y) . x
set y = f . x;
thus ((FuncAdd X,Y) . f,((FuncExtMult X,Y) . [(- 1r ),f])) . x = (f . x) + (((FuncExtMult X,Y) . [(- 1r ),f]) . x) by LOPBAN_1:3
.= (f . x) + ((- 1r ) * (f . x)) by Th3
.= (f . x) + (- (f . x)) by CLVECT_1:4
.= 0. Y by RLVECT_1:16
.= (FuncZero X,Y) . x by Th2 ; :: thesis: verum

end;

hence (FuncAdd X,Y) . f,((FuncExtMult X,Y) . [(- 1r ),f]) = FuncZero X,Y by FUNCT_2:113; :: thesis: verum