let R be comRing; :: thesis: for M, N, N1 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 N, the carrier of N1) st u is homogeneous holds
u * ((LMULT (M,N)) . [a,f]) = (LMULT (M,N1)) . [a,(u * f)]
let M, N, N1 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 N, the carrier of N1) st u is homogeneous holds
u * ((LMULT (M,N)) . [a,f]) = (LMULT (M,N1)) . [a,(u * f)]
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 N, the carrier of N1) st u is homogeneous holds
u * ((LMULT (M,N)) . [a,f]) = (LMULT (M,N1)) . [a,(u * f)]
let f be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: for u being Element of Funcs ( the carrier of N, the carrier of N1) st u is homogeneous holds
u * ((LMULT (M,N)) . [a,f]) = (LMULT (M,N1)) . [a,(u * f)]
let u be Element of Funcs ( the carrier of N, the carrier of N1); :: thesis: ( u is homogeneous implies u * ((LMULT (M,N)) . [a,f]) = (LMULT (M,N1)) . [a,(u * f)] )
assume A1: u is homogeneous ; :: thesis: u * ((LMULT (M,N)) . [a,f]) = (LMULT (M,N1)) . [a,(u * f)]
reconsider af = (LMULT (M,N)) . [a,f] as Element of Funcs ( the carrier of M, the carrier of N) ;
reconsider auf = (LMULT (M,N1)) . [a,(u * f)] as Element of Funcs ( the carrier of M, the carrier of N1) ;
for x being Element of the carrier of M holds (u * af) . x = auf . x

proof

let x be Element of the carrier of M; :: thesis: (u * af) . x = auf . x
reconsider fx = f . x as Element of the carrier of N ;
(u * af) . x = u . (af . x) by FUNCT_2:15
.= u . (a * fx) by Th16
.= a * (u . fx) by A1
.= a * ((u * f) . x) by FUNCT_2:15
.= auf . x by Th16 ;
hence (u * af) . x = auf . x ; :: thesis: verum

end;

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