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

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