let R be Ring; :: thesis: for M, N being LeftMod of R
for f being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,((LMULT (M,N)) . [(- (1. R)),f])) = 0_Funcs (M,N)
let M, N be LeftMod of R; :: thesis: for f being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,((LMULT (M,N)) . [(- (1. R)),f])) = 0_Funcs (M,N)
let f be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: (ADD (M,N)) . (f,((LMULT (M,N)) . [(- (1. R)),f])) = 0_Funcs (M,N)
set g = (LMULT (M,N)) . [(- (1. R)),f];
set F1 = (ADD (M,N)) . (f,((LMULT (M,N)) . [(- (1. R)),f]));
for x being Element of M holds ((ADD (M,N)) . (f,((LMULT (M,N)) . [(- (1. R)),f]))) . x = (0_Funcs (M,N)) . x

proof

let x be Element of M; :: thesis: ((ADD (M,N)) . (f,((LMULT (M,N)) . [(- (1. R)),f]))) . x = (0_Funcs (M,N)) . x
((LMULT (M,N)) . [(- (1. R)),f]) . x = (- (1. R)) * (f . x) by Th16
.= - (f . x) by VECTSP_1:14 ;
then ((ADD (M,N)) . (f,((LMULT (M,N)) . [(- (1. R)),f]))) . x = (f . x) + (- (f . x)) by Th15
.= ( the carrier of M --> (0. N)) . x by VECTSP_1:19
.= (0_Funcs (M,N)) . x by GRCAT_1:def 7 ;
hence ((ADD (M,N)) . (f,((LMULT (M,N)) . [(- (1. R)),f]))) . x = (0_Funcs (M,N)) . x ; :: thesis: verum

end;

hence (ADD (M,N)) . (f,((LMULT (M,N)) . [(- (1. R)),f])) = 0_Funcs (M,N) ; :: thesis: verum