theorem :: CAT_6:14

for C being CategoryStr holds
( C is composable iff CategoryStr(# the carrier of C, the composition of C #) is composable ) by Th12, Th13;