theorem :: CAT_1:31

for C being Category
for b, c being Object of C
for g being Morphism of b,c st Hom (b,c) <> {} holds
( g is monic iff for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 ) ;