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 = (FuncComp (AbGr M)) . ((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 = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g))
let f, g, h be Endomorphism of R,M; :: thesis: ( h = f * g implies AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g)) )
assume h = f * g ; :: thesis: AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g))
then for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) * (AbGr g)) . x by Lm33;
hence AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g)) by Th29; :: thesis: verum