let R be Ring; :: thesis: for M, N being LeftMod of R
for f, g being Element of Funcs ( the carrier of M, the carrier of N)
for a being Element of the carrier of R holds (LMULT (M,N)) . [a,((ADD (M,N)) . (f,g))] = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [a,g]))
let M, N be LeftMod of R; :: thesis: for f, g being Element of Funcs ( the carrier of M, the carrier of N)
for a being Element of the carrier of R holds (LMULT (M,N)) . [a,((ADD (M,N)) . (f,g))] = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [a,g]))
let f, g be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: for a being Element of the carrier of R holds (LMULT (M,N)) . [a,((ADD (M,N)) . (f,g))] = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [a,g]))
let a be Element of the carrier of R; :: thesis: (LMULT (M,N)) . [a,((ADD (M,N)) . (f,g))] = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [a,g]))
set af = (LMULT (M,N)) . [a,f];
set ag = (LMULT (M,N)) . [a,g];
set fg = (ADD (M,N)) . (f,g);
set F1 = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [a,g]));
set F2 = (LMULT (M,N)) . [a,((ADD (M,N)) . (f,g))];
for x being Element of M holds ((ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [a,g]))) . x = ((LMULT (M,N)) . [a,((ADD (M,N)) . (f,g))]) . x

proof

let x be Element of M; :: thesis: ((ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [a,g]))) . x = ((LMULT (M,N)) . [a,((ADD (M,N)) . (f,g))]) . x
A1: ((LMULT (M,N)) . [a,g]) . x = a * (g . x) by Th16;
A2: ((ADD (M,N)) . (f,g)) . x = (f . x) + (g . x) by Th15;
((ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [a,g]))) . x = (((LMULT (M,N)) . [a,f]) . x) + (((LMULT (M,N)) . [a,g]) . x) by Th15
.= (a * (f . x)) + (a * (g . x)) by Th16, A1
.= a * (((ADD (M,N)) . (f,g)) . x) by A2, VECTSP_1:def 14
.= ((LMULT (M,N)) . [a,((ADD (M,N)) . (f,g))]) . x by Th16 ;
hence ((ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [a,g]))) . x = ((LMULT (M,N)) . [a,((ADD (M,N)) . (f,g))]) . x ; :: thesis: verum

end;

hence (LMULT (M,N)) . [a,((ADD (M,N)) . (f,g))] = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [a,g])) ; :: thesis: verum