:: deftheorem Def13 defines comp MODCAT_1:def 14 :
for R being Ring
for V being LeftMod_DOMAIN of R
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 ) ) );