consider G1', G2' being LeftMod of such that
A8: F is Morphism of G1',G2' by Th16;
reconsider F' = F as Morphism of G1',G2' by A8;
consider G2, G3' being LeftMod of such that
A9: G is Morphism of G2,G3' by Th16;
G2 = dom G by A9, Def11;
then reconsider F' = F' as Morphism of G1',G2 by A1, Def11;
consider f' being Function of G1',G2 such that
A10: LModMorphismStr(# the Dom of F',the Cod of F',the Fun of F' #) = LModMorphismStr(# G1',G2,f' #) and
f' is linear by Th14;
reconsider G' = G as Morphism of G2,G3' by A9;
let S1, S2 be strict LModMorphism of R; :: 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
S1 = LModMorphismStr(# G1,G3,(g * f) #) ) & ( 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
S2 = LModMorphismStr(# G1,G3,(g * f) #) ) implies S1 = S2 )
assume that
A11: 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
S1 = LModMorphismStr(# G1,G3,(g * f) #) and
A12: 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
S2 = LModMorphismStr(# G1,G3,(g * f) #) ; :: thesis: S1 = S2
consider g' being Function of G2,G3' such that
A13: LModMorphismStr(# the Dom of G',the Cod of G',the Fun of G' #) = LModMorphismStr(# G2,G3',g' #) and
g' is linear by Th14;
thus S1 = LModMorphismStr(# G1',G3',(g' * f') #) by A11, A13, A10
.= S2 by A12, A13, A10 ; :: thesis: verum