:: deftheorem defines monomorphism CAT_7:def 5 :
for C being composable with_identities CategoryStr
for a, b being Object of C
for f being Morphism of a,b holds
( f is monomorphism iff ( Hom (a,b) <> {} & ( for c being Object of C st Hom (c,a) <> {} holds
for g1, g2 being Morphism of c,a st f * g1 = f * g2 holds
g1 = g2 ) ) );