let R be Ring; :: thesis: for M being AbGroup
for s being Function of R,(End_Ring M)
for a being Element of R
for x, y being Element of (AbGrLMod (M,s)) holds a * (x + y) = (a * x) + (a * y)
let M be AbGroup; :: thesis: for s being Function of R,(End_Ring M)
for a being Element of R
for x, y being Element of (AbGrLMod (M,s)) holds a * (x + y) = (a * x) + (a * y)
let s be Function of R,(End_Ring M); :: thesis: for a being Element of R
for x, y being Element of (AbGrLMod (M,s)) holds a * (x + y) = (a * x) + (a * y)
let a be Element of R; :: thesis: for x, y being Element of (AbGrLMod (M,s)) holds a * (x + y) = (a * x) + (a * y)
let x, y be Element of (AbGrLMod (M,s)); :: thesis: a * (x + y) = (a * x) + (a * y)
consider h being Endomorphism of M such that
A1: ( h = s . a & a * x = h . x ) by Def12;
consider h1 being Endomorphism of M such that
A2: ( h1 = s . a & a * y = h1 . y ) by Def12;
consider h2 being Endomorphism of M such that
A3: ( h2 = s . a & (LModlmult (M,s)) . (a,(x + y)) = h2 . (x + y) ) by Def12;
reconsider x1 = x, y1 = y as Element of M ;
a * (x + y) = h . (x1 + y1) by A1, A3
.= (h . x1) + (h . y1) by VECTSP_1:def 20
.= (a * x) + (a * y) by A1, A2 ;
hence a * (x + y) = (a * x) + (a * y) ; :: thesis: verum