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

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