let R be comRing; :: thesis: for M being LeftMod of R
for f, g, h being Endomorphism of R,M st h = f * g holds
AbGr h = (AbGr f) * (AbGr g)
let M be LeftMod of R; :: thesis: for f, g, h being Endomorphism of R,M st h = f * g holds
AbGr h = (AbGr f) * (AbGr g)
let f, g, h be Endomorphism of R,M; :: thesis: ( h = f * g implies AbGr h = (AbGr f) * (AbGr g) )
assume A1: h = f * g ; :: thesis: AbGr h = (AbGr f) * (AbGr g)
for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) * (AbGr g)) . x

proof

let x be Element of the carrier of (AbGr M); :: thesis: (AbGr h) . x = ((AbGr f) * (AbGr g)) . x
reconsider x2 = x as Element of the carrier of M ;
A2: (AbGr g) . x = g . x2 by Def26;
A3: (AbGr h) . x = h . x2 by Def26;
reconsider x0 = x as Element of the carrier of M ;
A4: (AbGr h) . x = f . (g . x0) by A1, A3, FUNCT_2:15;
reconsider y0 = g . x0 as Element of the carrier of (AbGr M) ;
reconsider y1 = y0 as Element of the carrier of M ;
(AbGr f) . y0 = f . y1 by Def26;
hence (AbGr h) . x = ((AbGr f) * (AbGr g)) . x by A4, A2, FUNCT_2:15; :: thesis: verum

end;

hence AbGr h = (AbGr f) * (AbGr g) ; :: thesis: verum