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)
for a, b being Element of the carrier of R holds (LMULT (M,N)) . [(a + b),f] = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [b,f]))
let M, N be LeftMod of R; :: thesis: for f being Element of Funcs ( the carrier of M, the carrier of N)
for a, b being Element of the carrier of R holds (LMULT (M,N)) . [(a + b),f] = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [b,f]))
let f be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: for a, b being Element of the carrier of R holds (LMULT (M,N)) . [(a + b),f] = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [b,f]))
let a, b be Element of the carrier of R; :: thesis: (LMULT (M,N)) . [(a + b),f] = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [b,f]))
set af = (LMULT (M,N)) . [a,f];
set bf = (LMULT (M,N)) . [b,f];
set abf = (LMULT (M,N)) . [(a + b),f];
set F1 = (LMULT (M,N)) . [(a + b),f];
set F2 = (ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [b,f]));
for x being Element of M holds ((LMULT (M,N)) . [(a + b),f]) . x = ((ADD (M,N)) . (((LMULT (M,N)) . [a,f]),((LMULT (M,N)) . [b,f]))) . x

proof

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

end;

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