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 8 :: thesis: f is monic
let f1, f2 be Morphism of C; :: according to CAT_1:def 7 :: 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 7 :: thesis: f opp is epi
let g1, g2 be Morphism of (C opp); :: according to CAT_1:def 8 :: 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