let f, g be strict RingMorphism; :: thesis: ( dom g = cod f implies ( dom (g * f) = dom f & cod (g * f) = cod g ) )
assume dom g = cod f ; :: thesis: ( 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 ; :: thesis: cod (g * f) = cod g
thus cod (g * f) = cod g by A1; :: thesis: verum