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

let x be Element of X; :: thesis: ((FuncAdd X,Y) . f,((FuncExtMult X,Y) . [(- 1),f])) . x = (FuncZero X,Y) . x
set y = f . x;
thus ((FuncAdd X,Y) . f,((FuncExtMult X,Y) . [(- 1),f])) . x = (f . x) + (((FuncExtMult X,Y) . [(- 1),f]) . x) by Th3
.= (f . x) + ((- 1) * (f . x)) by Th5
.= (f . x) + (- (f . x)) by RLVECT_1:29
.= 0. Y by RLVECT_1:16
.= (FuncZero X,Y) . x by FUNCOP_1:13 ; :: thesis: verum

end;

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