for C being composable with_identities CategoryStr
for a, b, c being Object of C
for f1 being Morphism of a,b
for f2 being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
( ( f1 is identity implies f2 * f1 = f2 ) & ( f2 is identity implies f2 * f1 = f1 ) )