consider G19, G29, G39 being Ring such that
A2:
G19 <= G29
and
A3:
( G29 <= G39 & RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) is Morphism of G29,G39 )
and
A4:
RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is Morphism of G19,G29
by A1, Th2;
consider g9 being Function of G29,G39 such that
A5:
RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G29,G39,g9 #)
and
A6:
g9 is linear
by A3, Lm7;
consider f9 being Function of G19,G29 such that
A7:
RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G19,G29,f9 #)
and
A8:
f9 is linear
by A2, A4, Lm7;
g9 * f9 is linear
by A6, A8, Th1;
then reconsider T9 = RingMorphismStr(# G19,G39,(g9 * f9) #) as strict RingMorphism by Lm5;
take
T9
; for G1, G2, G3 being Ring
for g being Function of G2,G3
for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
T9 = RingMorphismStr(# G1,G3,(g * f) #)
thus
for G1, G2, G3 being Ring
for g being Function of G2,G3
for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
T9 = RingMorphismStr(# G1,G3,(g * f) #)
by A5, A7; verum