let G1, G2, G3, G4 be Ring; for f being Morphism of G1,G2
for g being Morphism of G2,G3
for h being Morphism of G3,G4 st G1 <= G2 & G2 <= G3 & G3 <= G4 holds
h * (g * f) = (h * g) * f
let f be Morphism of G1,G2; for g being Morphism of G2,G3
for h being Morphism of G3,G4 st G1 <= G2 & G2 <= G3 & G3 <= G4 holds
h * (g * f) = (h * g) * f
let g be Morphism of G2,G3; for h being Morphism of G3,G4 st G1 <= G2 & G2 <= G3 & G3 <= G4 holds
h * (g * f) = (h * g) * f
let h be Morphism of G3,G4; ( G1 <= G2 & G2 <= G3 & G3 <= G4 implies h * (g * f) = (h * g) * f )
assume that
A1:
G1 <= G2
and
A2:
G2 <= G3
and
A3:
G3 <= G4
; h * (g * f) = (h * g) * f
consider f0 being Function of G1,G2 such that
A4:
f = RingMorphismStr(# G1,G2,f0 #)
by A1, Lm8;
consider h0 being Function of G3,G4 such that
A5:
h = RingMorphismStr(# G3,G4,h0 #)
by A3, Lm8;
consider g0 being Function of G2,G3 such that
A6:
g = RingMorphismStr(# G2,G3,g0 #)
by A2, Lm8;
A7:
cod g = G3
by A6;
A8:
dom h = G3
by A5;
then A9:
h * g = RingMorphismStr(# G2,G4,(h0 * g0) #)
by A6, A5, A7, Def9;
A10:
dom g = G2
by A6;
then A11:
dom (h * g) = G2
by A7, A8, Th8;
A12:
cod f = G2
by A4;
then A13:
cod (g * f) = G3
by A10, A7, Th8;
g * f = RingMorphismStr(# G1,G3,(g0 * f0) #)
by A4, A6, A12, A10, Def9;
then h * (g * f) =
RingMorphismStr(# G1,G4,(h0 * (g0 * f0)) #)
by A5, A8, A13, Def9
.=
RingMorphismStr(# G1,G4,((h0 * g0) * f0) #)
by RELAT_1:36
.=
(h * g) * f
by A4, A12, A9, A11, Def9
;
hence
h * (g * f) = (h * g) * f
; verum