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