:: deftheorem Def8 defines Morphism RINGCAT1:def 8 :
for G, H being Ring st G <= H holds
for b₃ being strict RingMorphism holds
( b₃ is Morphism of G,H iff ( dom b₃ = G & cod b₃ = H ) );