let f, g be strict RingMorphism; ( dom g = cod f implies ( dom (g * f) = dom f & cod (g * f) = cod g ) )
assume
dom g = cod f
; ( dom (g * f) = dom f & cod (g * f) = cod g )
then A1:
ex G1, G2, G3 being Ring ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = RingMorphismStr(# G1,G2,f0 #) & g = RingMorphismStr(# G2,G3,g0 #) & g * f = RingMorphismStr(# G1,G3,(g0 * f0) #) )
by Th7;
hence
dom (g * f) = dom f
; cod (g * f) = cod g
thus
cod (g * f) = cod g
by A1; verum