:: deftheorem Def27 defines comp GRCAT_1:def 29 :
for V being Group_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 ) ) );