let C be Category; :: thesis: for b, c being Object of C st Hom (b,c) <> {} holds
for f being Morphism of b,c holds
( f opp is epi iff f is monic )

let b, c be Object of C; :: thesis: ( Hom (b,c) <> {} implies for f being Morphism of b,c holds
( f opp is epi iff f is monic ) )

assume A1: Hom (b,c) <> {} ; :: thesis: for f being Morphism of b,c holds
( f opp is epi iff f is monic )

let f be Morphism of b,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 that
Hom ((c opp),(b opp)) <> {} and
A2: for a being Object of (C opp) st Hom ((b opp),a) <> {} holds
for g1, g2 being Morphism of b opp ,a st g1 * (f opp) = g2 * (f opp) holds
g1 = g2 ; :: according to CAT_1:def 15 :: thesis: f is monic
thus Hom (b,c) <> {} by A1; :: according to CAT_1:def 14 :: thesis: for b1 being Element of the carrier of C holds
( Hom (b1,b) = {} or for b2, b3 being Morphism of b1,b holds
( not f * b2 = f * b3 or b2 = b3 ) )

let a be Object of C; :: thesis: ( Hom (a,b) = {} or for b1, b2 being Morphism of a,b holds
( not f * b1 = f * b2 or b1 = b2 ) )

assume A3: Hom (a,b) <> {} ; :: thesis: for b1, b2 being Morphism of a,b holds
( not f * b1 = f * b2 or b1 = b2 )

let f1, f2 be Morphism of a,b; :: thesis: ( not f * f1 = f * f2 or f1 = f2 )
assume A4: f * f1 = f * f2 ; :: thesis: f1 = f2
reconsider g1 = f1 opp , g2 = f2 opp as Morphism of b opp ,a opp ;
A5: Hom ((b opp),(a opp)) <> {} by ;
g1 * (f opp) = f * f1 by Lm3, A1, A3
.= g2 * (f opp) by Lm3, A1, A3, A4 ;
then g1 = g2 by A2, A5;
hence f1 = g2 by
.= f2 by ;
:: thesis: verum
end;
assume that
A6: Hom (b,c) <> {} and
A7: for a being Object of C st Hom (a,b) <> {} holds
for f1, f2 being Morphism of a,b st f * f1 = f * f2 holds
f1 = f2 ; :: according to CAT_1:def 14 :: thesis: f opp is epi
thus Hom ((c opp),(b opp)) <> {} by ; :: according to CAT_1:def 15 :: thesis: for b1 being Element of the carrier of (C opp) holds
( Hom ((b opp),b1) = {} or for b2, b3 being Morphism of b opp ,b1 holds
( not b2 * (f opp) = b3 * (f opp) or b2 = b3 ) )

let a be Object of (C opp); :: thesis: ( Hom ((b opp),a) = {} or for b1, b2 being Morphism of b opp ,a holds
( not b1 * (f opp) = b2 * (f opp) or b1 = b2 ) )

assume A8: Hom ((b opp),a) <> {} ; :: thesis: for b1, b2 being Morphism of b opp ,a holds
( not b1 * (f opp) = b2 * (f opp) or b1 = b2 )

let g1, g2 be Morphism of b opp ,a; :: thesis: ( not g1 * (f opp) = g2 * (f opp) or g1 = g2 )
assume A9: g1 * (f opp) = g2 * (f opp) ; :: thesis: g1 = g2
Hom ((b opp),a) = Hom ((opp a),(opp (b opp))) by Th5
.= Hom ((opp a),b) ;
then ( opp g1 in Hom ((opp a),b) & opp g2 in Hom ((opp a),b) ) by ;
then reconsider f1 = opp g1, f2 = opp g2 as Morphism of opp a,b by CAT_1:def 5;
A10: Hom ((opp a),(opp (b opp))) <> {} by ;
f * f1 = (f1 opp) * (f opp) by A6, Lm3, A10
.= g2 * (f opp) by
.= (f2 opp) * (f opp) by
.= f * f2 by A6, Lm3, A10 ;
hence g1 = g2 by ; :: thesis: verum