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 ;

now

thus dom (f1 opp ) = cod (f opp ) by A3; :: thesis: ( dom (f2 opp ) = cod (f opp ) & cod (f1 opp ) = cod (f2 opp ) & (f1 opp ) * (f opp ) = (f2 opp ) * (f opp ) )
thus dom (f2 opp ) = cod (f opp ) by A4; :: thesis: ( cod (f1 opp ) = cod (f2 opp ) & (f1 opp ) * (f opp ) = (f2 opp ) * (f opp ) )
thus cod (f1 opp ) = cod (f2 opp ) by A2; :: thesis: (f1 opp ) * (f opp ) = (f2 opp ) * (f opp )
thus (f1 opp ) * (f opp ) = (f * f2) opp by A3, A5, Th17
.= (f2 opp ) * (f opp ) by A4, Th17 ; :: thesis: verum

end;

hence f1 = f2 by A1; :: thesis: verum

end;

assume A6: 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
A7: dom g1 = cod (f opp ) and
A8: dom g2 = cod (f opp ) and
A9: cod g1 = cod g2 and
A10: g1 * (f opp ) = g2 * (f opp ) ; :: thesis: g1 = g2
set f1 = opp g1;
set f2 = opp g2;

now

thus dom (opp g1) = dom (opp g2) by A9; :: thesis: ( cod (opp g1) = dom f & cod (opp g2) = dom f & f * (opp g1) = f * (opp g2) )
thus A11: cod (opp g1) = dom f by A7; :: thesis: ( cod (opp g2) = dom f & f * (opp g1) = f * (opp g2) )
thus A12: cod (opp g2) = dom f by A8; :: thesis: f * (opp g1) = f * (opp g2)
thus f * (opp g1) = (f * (opp g1)) opp
.= ((opp g1) opp ) * (f opp ) by A11, Th17
.= ((opp g2) opp ) * (f opp ) by A10
.= (f * (opp g2)) opp by A12, Th17
.= f * (opp g2) ; :: thesis: verum

end;

hence g1 = g2 by A6; :: thesis: verum