consider G1', G2, G3' being LeftMod of such that
A2: G is Morphism of G2,G3' and
A3: F is Morphism of G1',G2 by A1, Th18;
consider f' being Function of G1',G2 such that
A4: LModMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) = LModMorphismStr(# G1',G2,f' #) and
A5: f' is linear by A3, Th14;
consider g' being Function of G2,G3' such that
A6: LModMorphismStr(# the Dom of G,the Cod of G,the Fun of G #) = LModMorphismStr(# G2,G3',g' #) and
A7: g' is linear by A2, Th14;
g' * f' is linear by A7, A5, Th6;
then reconsider T' = LModMorphismStr(# G1',G3',(g' * f') #) as strict LModMorphism of R by Th12;
take T' ; :: thesis: for G1, G2, G3 being LeftMod of
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
T' = LModMorphismStr(# G1,G3,(g * f) #)
thus for G1, G2, G3 being LeftMod of
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
T' = LModMorphismStr(# G1,G3,(g * f) #) by A6, A4; :: thesis: verum