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 A2: for g1, g2 being Morphism of C st dom g1 = cod f & dom g2 = cod f & cod g1 = cod g2 & g1 * f = g2 * f holds
g1 = g2 ; :: according to CAT_1:def 8 :: 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 )
assume A3: Hom (b,c) <> {} ; :: thesis: ( not g1 * f = g2 * f or g1 = g2 )
then A4: ( dom g1 = b & dom g2 = b ) by Th23;
A5: cod f = b by A1, Th23;
A6: ( cod g1 = c & cod g2 = c ) by A3, Th23;
( g1 * f = g1 * f & g2 * f = g2 * f ) by A1, A3, Def13;
hence ( not g1 * f = g2 * f or g1 = g2 ) by A2, A4, A6, A5; :: 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
let g1, g2 be Morphism of C; :: according to CAT_1:def 8 :: thesis: ( dom g1 = cod f & dom g2 = cod f & cod g1 = cod g2 & g1 * f = g2 * f implies g1 = g2 )
assume that
A8: dom g1 = cod f and
A9: ( dom g2 = cod f & cod g1 = cod g2 ) ; :: thesis: ( not g1 * f = g2 * f or g1 = g2 )
set c = cod g1;
A10: cod f = b by A1, Th23;
then reconsider g1 = g1 as Morphism of b, cod g1 by A8, Th22;
reconsider g2 = g2 as Morphism of b, cod g1 by A9, A10, Th22;
A11: Hom (b,(cod g1)) <> {} by A8, A10, Th18;
then ( g1 * f = g1 * f & g2 * f = g2 * f ) by A1, Def13;
hence ( not g1 * f = g2 * f or g1 = g2 ) by A7, A11; :: thesis: verum