theorem Th13:
for
R being
Ring for
G1,
G2,
G3 being
LeftMod of
R for
G being
Morphism of
G2,
G3 for
F being
Morphism of
G1,
G2 for
g being
Function of
G2,
G3 for
f being
Function of
G1,
G2 st
G = LModMorphismStr(#
G2,
G3,
g #) &
F = LModMorphismStr(#
G1,
G2,
f #) holds
(
G *' F = LModMorphismStr(#
G1,
G3,
(g * f) #) &
G * F = LModMorphismStr(#
G1,
G3,
(g * f) #) )