:: deftheorem Def9 defines * RINGCAT1:def 9 :
for G, F being RingMorphism st dom G = cod F holds
for b₃ being strict RingMorphism holds
( b₃ = G * F iff 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
b₃ = RingMorphismStr(# G1,G3,(g * f) #) );