:: deftheorem Def2 defines are_composable CAT_6:def 2 :
for C being CategoryStr
for f1, f2 being morphism of C holds
( f1,f2 are_composable iff [f1,f2] in dom the composition of C );