let R be comRing; :: thesis: for M being LeftMod of R holds
( rho M is additive & rho M is homogeneous )
let M be LeftMod of R; :: thesis: ( rho M is additive & rho M is homogeneous )
reconsider EM = AbGrLMod ((AbGr M),(canHom M)) as LeftMod of R ;
for x being Element of the carrier of M
for a being Element of R holds (rho M) . (a * x) = a * ((rho M) . x)

proof

let x be Element of the carrier of M; :: thesis: for a being Element of R holds (rho M) . (a * x) = a * ((rho M) . x)
let a be Element of R; :: thesis: (rho M) . (a * x) = a * ((rho M) . x)
reconsider z = a * x as Element of the carrier of M ;
consider F being Endomorphism of (AbGr M) such that
A7: ( F = (canHom M) . a & (LModlmult ((AbGr M),(canHom M))) . (a,x) = F . x ) by Def12;
consider f being Endomorphism of R,M such that
A8: ( f = (curry the lmult of M) . a & (canHom M) . a = AbGr f ) by Def27;
reconsider x1 = x as Element of the carrier of (AbGr M) ;
reconsider x2 = x1 as Element of the carrier of M ;
(AbGr f) . x1 = f . x2 by Def26;
hence (rho M) . (a * x) = a * ((rho M) . x) by LOPBAN_8:7, A8, A7; :: thesis: verum

end;

hence ( rho M is additive & rho M is homogeneous ) ; :: thesis: verum