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

proof

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

end;

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