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, Th18;
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 linear by A3, Th14;
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 linear by A2, Th14;
g9 * f9 is linear by A7, A5, Th6;
then reconsider T9 = LModMorphismStr(# G19,G39,(g9 * f9) #) as strict LModMorphism of R by Th12;
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