:: deftheorem Def21 defines comp RINGCAT1:def 23 :
for V being Ring_DOMAIN
for b₂ being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) holds
( b₂ = comp V iff ( ( for g, f being Element of Morphs V holds
( [g,f] in dom b₂ iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b₂ holds
b₂ . (g,f) = g * f ) ) );