:: deftheorem Def10 defines *' RINGCAT1:def 10 :
for G1, G2, G3 being Ring
for G being Morphism of G2,G3
for F being Morphism of G1,G2 st G1 <= G2 & G2 <= G3 holds
G *' F = G * F;