let R be Ring; :: thesis: for X being set
for f being Element of Funcs (X, the carrier of R) holds (ADD (X,R)) . (f,((LMULT (X,R)) . ((- (1. R)),f))) = 0_Funcs (X,R)
let X be set ; :: thesis: for f being Element of Funcs (X, the carrier of R) holds (ADD (X,R)) . (f,((LMULT (X,R)) . ((- (1. R)),f))) = 0_Funcs (X,R)
let f be Element of Funcs (X, the carrier of R); :: thesis: (ADD (X,R)) . (f,((LMULT (X,R)) . ((- (1. R)),f))) = 0_Funcs (X,R)
set g = (LMULT (X,R)) . ((- (1. R)),f);
set F1 = (ADD (X,R)) . (f,((LMULT (X,R)) . ((- (1. R)),f)));
B1: ( dom ((ADD (X,R)) . (f,((LMULT (X,R)) . ((- (1. R)),f)))) = X & dom ((LMULT (X,R)) . ((- (1. R)),f)) = X ) by FUNCT_2:92;
for x being object st x in X holds
((ADD (X,R)) . (f,((LMULT (X,R)) . ((- (1. R)),f)))) . x = (0_Funcs (X,R)) . x

proof

let x be object ; :: thesis: ( x in X implies ((ADD (X,R)) . (f,((LMULT (X,R)) . ((- (1. R)),f)))) . x = (0_Funcs (X,R)) . x )
assume A0: x in X ; :: thesis: ((ADD (X,R)) . (f,((LMULT (X,R)) . ((- (1. R)),f)))) . x = (0_Funcs (X,R)) . x
then reconsider fx = f . x as Element of R by FUNCT_2:5;
(- (1. R)) * fx = - ((1. R) * fx) by VECTSP_1:9
.= - fx ;
then ((LMULT (X,R)) . ((- (1. R)),f)) . x = - fx by A0, Th2;
then ((ADD (X,R)) . (f,((LMULT (X,R)) . ((- (1. R)),f)))) . x = fx + (- fx) by A0, Th1
.= 0. R by RLVECT_1:5
.= (0_Funcs (X,R)) . x by A0, FUNCOP_1:7 ;
hence ((ADD (X,R)) . (f,((LMULT (X,R)) . ((- (1. R)),f)))) . x = (0_Funcs (X,R)) . x ; :: thesis: verum

end;

hence (ADD (X,R)) . (f,((LMULT (X,R)) . ((- (1. R)),f))) = 0_Funcs (X,R) by B1; :: thesis: verum