let R be comRing; :: thesis: for M being LeftMod of R
for a being Element of R holds (curry the lmult of M) . a is Endomorphism of R,M
let M be LeftMod of R; :: thesis: for a being Element of R holds (curry the lmult of M) . a is Endomorphism of R,M
let a be Element of R; :: thesis: (curry the lmult of M) . a is Endomorphism of R,M
set f = (curry the lmult of M) . a;
A1: for m1, m2 being Element of M holds ((curry the lmult of M) . a) . (m1 + m2) = (((curry the lmult of M) . a) . m1) + (((curry the lmult of M) . a) . m2)

proof

let m1, m2 be Element of M; :: thesis: ((curry the lmult of M) . a) . (m1 + m2) = (((curry the lmult of M) . a) . m1) + (((curry the lmult of M) . a) . m2)
A2: ( a * m1 = ((curry the lmult of M) . a) . m1 & a * m2 = ((curry the lmult of M) . a) . m2 ) by LOPBAN_8:7;
((curry the lmult of M) . a) . (m1 + m2) = a * (m1 + m2) by LOPBAN_8:7
.= (((curry the lmult of M) . a) . m1) + (((curry the lmult of M) . a) . m2) by A2, VECTSP_1:def 14 ;
hence ((curry the lmult of M) . a) . (m1 + m2) = (((curry the lmult of M) . a) . m1) + (((curry the lmult of M) . a) . m2) ; :: thesis: verum

end;

for b being Element of R
for m being Element of M holds ((curry the lmult of M) . a) . (b * m) = b * (((curry the lmult of M) . a) . m)

proof

let b be Element of R; :: thesis: for m being Element of M holds ((curry the lmult of M) . a) . (b * m) = b * (((curry the lmult of M) . a) . m)
let m be Element of M; :: thesis: ((curry the lmult of M) . a) . (b * m) = b * (((curry the lmult of M) . a) . m)
((curry the lmult of M) . a) . (b * m) = a * (b * m) by LOPBAN_8:7
.= (a * b) * m by VECTSP_1:def 16
.= b * (a * m) by VECTSP_1:def 16
.= b * (((curry the lmult of M) . a) . m) by LOPBAN_8:7 ;
hence ((curry the lmult of M) . a) . (b * m) = b * (((curry the lmult of M) . a) . m) ; :: thesis: verum

end;

then (curry the lmult of M) . a is homogeneous ;
hence (curry the lmult of M) . a is Endomorphism of R,M by A1, Def10, VECTSP_1:def 20; :: thesis: verum