let R be comRing; :: thesis: for M, N, M1 being LeftMod of R
for a being Element of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for u being Element of Funcs ( the carrier of M1, the carrier of M) holds ((LMULT (M,N)) . [a,f]) * u = (LMULT (M1,N)) . [a,(f * u)]
let M, N, M1 be LeftMod of R; :: thesis: for a being Element of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for u being Element of Funcs ( the carrier of M1, the carrier of M) holds ((LMULT (M,N)) . [a,f]) * u = (LMULT (M1,N)) . [a,(f * u)]
let a be Element of R; :: thesis: for f being Element of Funcs ( the carrier of M, the carrier of N)
for u being Element of Funcs ( the carrier of M1, the carrier of M) holds ((LMULT (M,N)) . [a,f]) * u = (LMULT (M1,N)) . [a,(f * u)]
let f be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: for u being Element of Funcs ( the carrier of M1, the carrier of M) holds ((LMULT (M,N)) . [a,f]) * u = (LMULT (M1,N)) . [a,(f * u)]
let u be Element of Funcs ( the carrier of M1, the carrier of M); :: thesis: ((LMULT (M,N)) . [a,f]) * u = (LMULT (M1,N)) . [a,(f * u)]
reconsider af = (LMULT (M,N)) . [a,f] as Element of Funcs ( the carrier of M, the carrier of N) ;
reconsider fu = f * u, afu = (LMULT (M1,N)) . [a,(f * u)] as Element of Funcs ( the carrier of M1, the carrier of N) ;
for x being Element of the carrier of M1 holds (af * u) . x = afu . x

proof

let x be Element of the carrier of M1; :: thesis: (af * u) . x = afu . x
reconsider ux = u . x as Element of the carrier of M ;
A1: fu . x = f . ux by FUNCT_2:15;
(af * u) . x = af . ux by FUNCT_2:15
.= a * ((f * u) . x) by A1, Th16
.= afu . x by Th16 ;
hence (af * u) . x = afu . x ; :: thesis: verum

end;

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