consider G19, G2, G39 being LeftMod of R such that
A2: G is Morphism of G2,G39 and
A3: F is Morphism of G19,G2 by A1, Th11;
consider f9 being Function of G19,G2 such that
A4: LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G19,G2,f9 #) and
A5: ( f9 is additive & f9 is homogeneous ) by A3, Th7;
consider g9 being Function of G2,G39 such that
A6: LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G39,g9 #) and
A7: ( g9 is additive & g9 is homogeneous ) by A2, Th7;
( g9 * f9 is additive & g9 * f9 is homogeneous ) by A7, A5, Th2;
then reconsider T9 = LModMorphismStr(# G19,G39,(g9 * f9) #) as strict LModMorphism of R by Th6;
take T9 ; :: thesis: for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
T9 = LModMorphismStr(# G1,G3,(g * f) #)
thus for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
T9 = LModMorphismStr(# G1,G3,(g * f) #) by A6, A4; :: thesis: verum