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

now :: thesis: for x being Element of X holds ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- jj),f]))) . x = (FuncZero (X,Y)) . x

let x be Element of X; :: thesis: ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- jj),f]))) . x = (FuncZero (X,Y)) . x
set y = f . x;
thus ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- jj),f]))) . x = (f . x) + (((FuncExtMult (X,Y)) . [(- jj),f]) . x) by Th1
.= (f . x) + ((- 1) * (f . x)) by Th2
.= (f . x) + (- (f . x)) by RLVECT_1:16
.= 0. Y by RLVECT_1:5
.= (FuncZero (X,Y)) . x by FUNCOP_1:7 ; :: thesis: verum

end;

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