theorem Th29: :: LMOD_XX1:29

for R being comRing
for M being LeftMod of R
for f, g, h being Endomorphism of R,M holds
( AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g)) iff for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) * (AbGr g)) . x )