let C be Category; :: thesis: for f being Morphism of C holds
( f opp is epi iff f is monic )
let f be Morphism of C; :: thesis: ( f opp is epi iff f is monic )
thus ( f opp is epi implies f is monic ) :: thesis: ( f is monic implies f opp is epi )

proof

assume A1: for g1, g2 being Morphism of (C opp ) st dom g1 = cod (f opp ) & dom g2 = cod (f opp ) & cod g1 = cod g2 & g1 * (f opp ) = g2 * (f opp ) holds
g1 = g2 ; :: according to CAT_1:def 11 :: thesis: f is monic
let f1, f2 be Morphism of C; :: according to CAT_1:def 10 :: thesis: ( not dom f1 = dom f2 or not cod f1 = dom f or not cod f2 = dom f or not f * f1 = f * f2 or f1 = f2 )
assume that
A2: dom f1 = dom f2 and
A3: cod f1 = dom f and
A4: cod f2 = dom f and
A5: f * f1 = f * f2 ; :: thesis: f1 = f2
set g1 = f1 opp ;
set g2 = f2 opp ;
A6: ( dom (f1 opp ) = cod (f opp ) & dom (f2 opp ) = cod (f opp ) ) by A3, A4;
A7: cod (f1 opp ) = cod (f2 opp ) by A2;
(f1 opp ) * (f opp ) = (f * f2) opp by A3, A5, Th17
.= (f2 opp ) * (f opp ) by A4, Th17 ;
hence f1 = f2 by A1, A6, A7; :: thesis: verum

end;

assume A8: for f1, f2 being Morphism of C st dom f1 = dom f2 & cod f1 = dom f & cod f2 = dom f & f * f1 = f * f2 holds
f1 = f2 ; :: according to CAT_1:def 10 :: thesis: f opp is epi
let g1, g2 be Morphism of (C opp ); :: according to CAT_1:def 11 :: thesis: ( not dom g1 = cod (f opp ) or not dom g2 = cod (f opp ) or not cod g1 = cod g2 or not g1 * (f opp ) = g2 * (f opp ) or g1 = g2 )
assume that
A9: dom g1 = cod (f opp ) and
A10: dom g2 = cod (f opp ) and
A11: cod g1 = cod g2 and
A12: g1 * (f opp ) = g2 * (f opp ) ; :: thesis: g1 = g2
set f1 = opp g1;
set f2 = opp g2;
A13: ( dom (opp g1) = dom (opp g2) & cod (opp g1) = dom f ) by A9, A11;
A14: cod (opp g2) = dom f by A10;
A15: cod (opp g1) = dom f by A9;
A16: cod (opp g2) = dom f by A10;
f * (opp g1) = (f * (opp g1)) opp
.= ((opp g1) opp ) * (f opp ) by A15, Th17
.= ((opp g2) opp ) * (f opp ) by A12
.= (f * (opp g2)) opp by A14, Th17
.= f * (opp g2) ;
hence g1 = g2 by A8, A13, A16; :: thesis: verum