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 )
thus ( f opp is monic implies f is epi ) :: thesis: ( f is epi implies f opp is monic )

proof

assume A1: 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 10 :: thesis: f is epi
let g1, g2 be Morphism of C; :: according to CAT_1:def 11 :: 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
A2: ( dom g1 = cod f & dom g2 = cod f ) and
A3: ( cod g1 = cod g2 & g1 * f = g2 * f ) ; :: thesis: g1 = g2
( dom (f opp ) = cod f & dom (g1 opp ) = cod g1 & dom (g2 opp ) = cod g2 & cod (g1 opp ) = dom g1 & cod (g2 opp ) = dom g2 & (g1 * f) opp = (f opp ) * (g1 opp ) & (g2 * f) opp = (f opp ) * (g2 opp ) & g1 opp = g1 & g2 opp = g2 ) by A2, Th17;
hence g1 = g2 by A1, A2, A3; :: thesis: verum

end;

assume A4: 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 11 :: thesis: f opp is monic
let f1, f2 be Morphism of (C opp ); :: according to CAT_1:def 10 :: 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
A5: dom f1 = dom f2 and
A6: ( cod f1 = dom (f opp ) & cod f2 = dom (f opp ) ) and
A7: (f opp ) * f1 = (f opp ) * f2 ; :: thesis: f1 = f2
set g1 = opp f1;
set g2 = opp f2;
A8: ( dom (opp f1) = cod ((opp f1) opp ) & dom (opp f2) = cod ((opp f2) opp ) & dom (f opp ) = cod f ) ;
then ( cod (opp f1) = dom ((opp f1) opp ) & cod (opp f2) = dom ((opp f2) opp ) & ((opp f1) * f) opp = (opp f1) * f & ((opp f2) * f) opp = (opp f2) * f & (f opp ) * ((opp f1) opp ) = ((opp f1) * f) opp & (f opp ) * ((opp f2) opp ) = ((opp f2) * f) opp ) by A6, Th17;
hence f1 = f2 by A4, A5, A6, A7, A8; :: thesis: verum