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

proof

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

end;

assume A7: 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: f opp is monic
let f1, f2 be Morphism of (C opp); :: according to CAT_1:def 7 :: thesis: ( not dom f1 = dom f2 or not cod f1 = dom (f opp) or not cod f2 = dom (f opp) or not (f opp) * f1 = (f opp) * f2 or f1 = f2 )
assume that
A8: dom f1 = dom f2 and
A9: cod f1 = dom (f opp) and
A10: cod f2 = dom (f opp) and
A11: (f opp) * f1 = (f opp) * f2 ; :: thesis: f1 = f2
set g1 = opp f1;
set g2 = opp f2;
A12: dom (opp f2) = cod ((opp f2) opp) ;
then A13: (f opp) * ((opp f2) opp) = ((opp f2) * f) opp by A10, A1, Th17;
A14: ( cod (opp f1) = dom ((opp f1) opp) & cod (opp f2) = dom ((opp f2) opp) ) ;
A15: dom (opp f1) = cod ((opp f1) opp) ;
then (f opp) * ((opp f1) opp) = ((opp f1) * f) opp by A9, A1, Th17;
hence f1 = f2 by A7, A8, A9, A10, A11, A15, A12, A14, A13; :: thesis: verum