let G1, G2, G3, G4 be AddGroup; 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; 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; for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f
let h be strict Morphism of G3,G4; h * (g * f) = (h * g) * f
consider f0 being Function of G1,G2 such that
A1:
f = GroupMorphismStr(# G1,G2,f0 #)
by Th13;
consider g0 being Function of G2,G3 such that
A2:
g = GroupMorphismStr(# G2,G3,g0 #)
by Th13;
consider h0 being Function of G3,G4 such that
A3:
h = GroupMorphismStr(# G3,G4,h0 #)
by Th13;
A4:
h * g = GroupMorphismStr(# G2,G4,(h0 * g0) #)
by A2, A3, Th18;
g * f = GroupMorphismStr(# G1,G3,(g0 * f0) #)
by A1, A2, Th18;
then h * (g * f) =
GroupMorphismStr(# G1,G4,(h0 * (g0 * f0)) #)
by A3, Th18
.=
GroupMorphismStr(# G1,G4,((h0 * g0) * f0) #)
by RELAT_1:36
.=
(h * g) * f
by A1, A4, Th18
;
hence
h * (g * f) = (h * g) * f
; verum