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 b₁ being Element of the carrier of C holds
( Hom (b₁,b) = {} or for b₂, b₃ being Morphism of b₁,b holds
( not f * b₂ = f * b₃ or b₂ = b₃ ) )
let a be Object of C; :: thesis: ( Hom (a,b) = {} or for b₁, b₂ being Morphism of a,b holds
( not f * b₁ = f * b₂ or b₁ = b₂ ) )
assume A3: Hom (a,b) <> {} ; :: thesis: for b₁, b₂ being Morphism of a,b holds
( not f * b₁ = f * b₂ or b₁ = b₂ )
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 A3, Th4;
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 Def6, A3
.= f2 by Def6, A3 ;
:: 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 A6, Th4; :: according to CAT_1:def 15 :: thesis: for b₁ being Element of the carrier of (C opp) holds
( Hom ((b opp),b₁) = {} or for b₂, b₃ being Morphism of b opp ,b₁ holds
( not b₂ * (f opp) = b₃ * (f opp) or b₂ = b₃ ) )
let a be Object of (C opp); :: thesis: ( Hom ((b opp),a) = {} or for b₁, b₂ being Morphism of b opp ,a holds
( not b₁ * (f opp) = b₂ * (f opp) or b₁ = b₂ ) )
assume A8: Hom ((b opp),a) <> {} ; :: thesis: for b₁, b₂ being Morphism of b opp ,a holds
( not b₁ * (f opp) = b₂ * (f opp) or b₁ = b₂ )
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 A8, CAT_1:def 5;
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 A8, Th5;
f * f1 = (f1 opp) * (f opp) by A6, Lm3, A10
.= g2 * (f opp) by A9, Def6, A10
.= (f2 opp) * (f opp) by Def6, A10
.= f * f2 by A6, Lm3, A10 ;
hence g1 = g2 by A7, A10; :: thesis: verum