let C be Category; :: thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is epi iff for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 )
let a, b be Object of C; :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is epi iff for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 )
let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} implies ( f is epi iff for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 ) )
assume A1: Hom (a,b) <> {} ; :: thesis: ( f is epi iff for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 )
thus ( f is epi implies for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 ) :: thesis: ( ( for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 ) implies f is epi )

proof

assume that
Hom (a,b) <> {} and
A2: 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 ; :: according to CAT_1:def 15 :: thesis: for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2
let c be Object of C; :: thesis: for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2
let g1, g2 be Morphism of b,c; :: thesis: ( Hom (b,c) <> {} & g1 * f = g2 * f implies g1 = g2 )
thus ( Hom (b,c) <> {} & g1 * f = g2 * f implies g1 = g2 ) by A2; :: thesis: verum

end;

assume A7: for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 ; :: thesis: f is epi
thus Hom (a,b) <> {} by A1; :: according to CAT_1:def 15 :: thesis: 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
thus 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 by A7; :: thesis: verum