consider G19, G29 being LeftMod of R such that
A8: F is Morphism of G19,G29 by Th9;
reconsider F9 = F as Morphism of G19,G29 by A8;
consider G2, G39 being LeftMod of R such that
A9: G is Morphism of G2,G39 by Th9;
G2 = dom G by A9, Def8;
then reconsider F9 = F9 as Morphism of G19,G2 by A1, Def8;
consider f9 being Function of G19,G2 such that
A10: LModMorphismStr(# the Dom of F9, the Cod of F9, the Fun of F9 #) = LModMorphismStr(# G19,G2,f9 #) and
( f9 is additive & f9 is homogeneous ) by Th7;
reconsider G9 = G as Morphism of G2,G39 by A9;
let S1, S2 be strict LModMorphism of R; :: 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
S1 = LModMorphismStr(# G1,G3,(g * f) #) ) & ( 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
S2 = LModMorphismStr(# G1,G3,(g * f) #) ) implies S1 = S2 )
assume that
A11: 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
S1 = LModMorphismStr(# G1,G3,(g * f) #) and
A12: 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
S2 = LModMorphismStr(# G1,G3,(g * f) #) ; :: thesis: S1 = S2
consider g9 being Function of G2,G39 such that
A13: LModMorphismStr(# the Dom of G9, the Cod of G9, the Fun of G9 #) = LModMorphismStr(# G2,G39,g9 #) and
( g9 is additive & g9 is homogeneous ) by Th7;
thus S1 = LModMorphismStr(# G19,G39,(g9 * f9) #) by A11, A13, A10
.= S2 by A12, A13, A10 ; :: thesis: verum