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:1
.= (f . x) + ((- 1r) * (f . x)) by Th3
.= (f . x) + (- (f . x)) by CLVECT_1:3
.= 0. Y by RLVECT_1:5
.= (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:63; :: thesis: verum