let R be Ring; :: thesis: for G1, G2, G3, G4 being LeftMod of R

for f being strict Morphism of G1,G2

for g being strict Morphism of G2,G3

for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f

let G1, G2, G3, G4 be LeftMod of R; :: thesis: for f being strict Morphism of G1,G2

for g being strict Morphism of G2,G3

for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f

let f be strict Morphism of G1,G2; :: thesis: for g being strict Morphism of G2,G3

for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f

let g be strict Morphism of G2,G3; :: thesis: for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f

let h be strict Morphism of G3,G4; :: thesis: h * (g * f) = (h * g) * f

consider f0 being Function of G1,G2 such that

A1: f = LModMorphismStr(# G1,G2,f0 #) by Th8;

consider g0 being Function of G2,G3 such that

A2: g = LModMorphismStr(# G2,G3,g0 #) by Th8;

consider h0 being Function of G3,G4 such that

A3: h = LModMorphismStr(# G3,G4,h0 #) by Th8;

A4: h *' g = LModMorphismStr(# G2,G4,(h0 * g0) #) by A2, A3, Th13;

g *' f = LModMorphismStr(# G1,G3,(g0 * f0) #) by A1, A2, Th13;

then h * (g * f) = LModMorphismStr(# G1,G4,(h0 * (g0 * f0)) #) by A3, Th13

.= LModMorphismStr(# G1,G4,((h0 * g0) * f0) #) by RELAT_1:36

.= (h * g) * f by A1, A4, Th13 ;

hence h * (g * f) = (h * g) * f ; :: thesis: verum

for f being strict Morphism of G1,G2

for g being strict Morphism of G2,G3

for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f

let G1, G2, G3, G4 be LeftMod of R; :: thesis: for f being strict Morphism of G1,G2

for g being strict Morphism of G2,G3

for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f

let f be strict Morphism of G1,G2; :: thesis: for g being strict Morphism of G2,G3

for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f

let g be strict Morphism of G2,G3; :: thesis: for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f

let h be strict Morphism of G3,G4; :: thesis: h * (g * f) = (h * g) * f

consider f0 being Function of G1,G2 such that

A1: f = LModMorphismStr(# G1,G2,f0 #) by Th8;

consider g0 being Function of G2,G3 such that

A2: g = LModMorphismStr(# G2,G3,g0 #) by Th8;

consider h0 being Function of G3,G4 such that

A3: h = LModMorphismStr(# G3,G4,h0 #) by Th8;

A4: h *' g = LModMorphismStr(# G2,G4,(h0 * g0) #) by A2, A3, Th13;

g *' f = LModMorphismStr(# G1,G3,(g0 * f0) #) by A1, A2, Th13;

then h * (g * f) = LModMorphismStr(# G1,G4,(h0 * (g0 * f0)) #) by A3, Th13

.= LModMorphismStr(# G1,G4,((h0 * g0) * f0) #) by RELAT_1:36

.= (h * g) * f by A1, A4, Th13 ;

hence h * (g * f) = (h * g) * f ; :: thesis: verum