let R be Ring; :: thesis: for M being AbGroup
for s being Function of R,(End_Ring M)
for a, b being Element of R
for x being Element of (AbGrLMod (M,s)) st s is RingHomomorphism holds
(a * b) * x = a * (b * x)
let M be AbGroup; :: thesis: for s being Function of R,(End_Ring M)
for a, b being Element of R
for x being Element of (AbGrLMod (M,s)) st s is RingHomomorphism holds
(a * b) * x = a * (b * x)
let s be Function of R,(End_Ring M); :: thesis: for a, b being Element of R
for x being Element of (AbGrLMod (M,s)) st s is RingHomomorphism holds
(a * b) * x = a * (b * x)
let a, b be Element of R; :: thesis: for x being Element of (AbGrLMod (M,s)) st s is RingHomomorphism holds
(a * b) * x = a * (b * x)
let x be Element of (AbGrLMod (M,s)); :: thesis: ( s is RingHomomorphism implies (a * b) * x = a * (b * x) )
assume A1: s is RingHomomorphism ; :: thesis: (a * b) * x = a * (b * x)
consider h being Endomorphism of M such that
A2: ( h = s . (a * b) & (a * b) * x = h . x ) by Def12;
consider h2 being Endomorphism of M such that
A3: ( h2 = s . b & b * x = h2 . x ) by Def12;
consider h3 being Endomorphism of M such that
A4: ( h3 = s . a & a * (b * x) = h3 . (b * x) ) by Def12;
s . a in set_End M ;
then consider ha being Function of the carrier of M, the carrier of M such that
A5: ( ha = s . a & ha is Endomorphism of M ) ;
s . b in set_End M ;
then consider hb being Function of the carrier of M, the carrier of M such that
A6: ( hb = s . b & hb is Endomorphism of M ) ;
A7: h = (s . a) * (s . b) by A2, A1, GROUP_6:def 6
.= (FuncComp M) . (ha,hb) by A5, A6, Th6 ;
reconsider h = h, ha = ha, hb = hb as Element of Funcs ( the carrier of M, the carrier of M) by FUNCT_2:9;
reconsider x1 = x as Element of the carrier of M ;
(a * b) * x = (ha * hb) . x1 by Def4, A2, A7
.= a * (b * x) by A4, A5, A3, A6, FUNCT_2:15 ;
hence (a * b) * x = a * (b * x) ; :: thesis: verum