for C being category
for a, b, c being Object of C
for f1 being Morphism of a,b
for f2 being Morphism of b,c st f2 * f1 is monomorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds
f1 is monomorphism