consider G1', G2', G3' being Ring such that
A2: G1' <= G2' and
A3: ( G2' <= G3' & RingMorphismStr(# the Dom of G,the Cod of G,the Fun of G #) is Morphism of G2',G3' ) and
A4: RingMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) is Morphism of G1',G2' by A1, Th5;
consider g' being Function of G2',G3' such that
A5: RingMorphismStr(# the Dom of G,the Cod of G,the Fun of G #) = RingMorphismStr(# G2',G3',g' #) and
A6: g' is linear by A3, Lm7;
consider f' being Function of G1',G2' such that
A7: RingMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) = RingMorphismStr(# G1',G2',f' #) and
A8: f' is linear by A2, A4, Lm7;
g' * f' is linear by A6, A8, Th3;
then reconsider T' = RingMorphismStr(# G1',G3',(g' * f') #) as strict RingMorphism by Lm5;
take T' ; :: thesis: 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
T' = 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
T' = RingMorphismStr(# G1,G3,(g * f) #) by A5, A7; :: thesis: verum