let C be Category; :: thesis: for c being Object of C holds

( c opp is initial iff c is terminal )

let c be Object of C; :: thesis: ( c opp is initial iff c is terminal )

thus ( c opp is initial implies c is terminal ) :: thesis: ( c is terminal implies c opp is initial )

let b be Object of (C opp); :: according to CAT_1:def 19 :: thesis: ( not Hom ((c opp),b) = {} & ex b_{1} being Morphism of c opp ,b st

for b_{2} being Morphism of c opp ,b holds b_{1} = b_{2} )

consider f being Morphism of opp b,c such that

A7: for g being Morphism of opp b,c holds f = g by A6;

A8: (opp b) opp = b ;

A9: Hom ((opp b),c) <> {} by A6;

reconsider f9 = f opp as Morphism of c opp ,b ;

thus A10: Hom ((c opp),b) <> {} by A8, Th4, A9; :: thesis: ex b_{1} being Morphism of c opp ,b st

for b_{2} being Morphism of c opp ,b holds b_{1} = b_{2}

take f9 ; :: thesis: for b_{1} being Morphism of c opp ,b holds f9 = b_{1}

let g be Morphism of c opp ,b; :: thesis: f9 = g

opp g is Morphism of opp b, opp (c opp) by A10, Th13;

hence g = f by A7

.= f9 by Def6, A9 ;

:: thesis: verum

( c opp is initial iff c is terminal )

let c be Object of C; :: thesis: ( c opp is initial iff c is terminal )

thus ( c opp is initial implies c is terminal ) :: thesis: ( c is terminal implies c opp is initial )

proof

assume A6:
c is terminal
; :: thesis: c opp is initial
assume A1:
c opp is initial
; :: thesis: c is terminal

let b be Object of C; :: according to CAT_1:def 18 :: thesis: ( not Hom (b,c) = {} & ex b_{1} being Morphism of b,c st

for b_{2} being Morphism of b,c holds b_{1} = b_{2} )

consider f being Morphism of c opp ,b opp such that

A2: for g being Morphism of c opp ,b opp holds f = g by A1;

A3: ( opp (b opp) = b & opp (c opp) = c ) ;

A4: Hom ((c opp),(b opp)) <> {} by A1;

reconsider f9 = opp f as Morphism of b,c ;

thus A5: Hom (b,c) <> {} by A3, Th5, A4; :: thesis: ex b_{1} being Morphism of b,c st

for b_{2} being Morphism of b,c holds b_{1} = b_{2}

take f9 ; :: thesis: for b_{1} being Morphism of b,c holds f9 = b_{1}

let g be Morphism of b,c; :: thesis: f9 = g

g opp = f by A2;

hence g = f by A5, Def6

.= f9 by Def7, A4 ;

:: thesis: verum

end;let b be Object of C; :: according to CAT_1:def 18 :: thesis: ( not Hom (b,c) = {} & ex b

for b

consider f being Morphism of c opp ,b opp such that

A2: for g being Morphism of c opp ,b opp holds f = g by A1;

A3: ( opp (b opp) = b & opp (c opp) = c ) ;

A4: Hom ((c opp),(b opp)) <> {} by A1;

reconsider f9 = opp f as Morphism of b,c ;

thus A5: Hom (b,c) <> {} by A3, Th5, A4; :: thesis: ex b

for b

take f9 ; :: thesis: for b

let g be Morphism of b,c; :: thesis: f9 = g

g opp = f by A2;

hence g = f by A5, Def6

.= f9 by Def7, A4 ;

:: thesis: verum

let b be Object of (C opp); :: according to CAT_1:def 19 :: thesis: ( not Hom ((c opp),b) = {} & ex b

for b

consider f being Morphism of opp b,c such that

A7: for g being Morphism of opp b,c holds f = g by A6;

A8: (opp b) opp = b ;

A9: Hom ((opp b),c) <> {} by A6;

reconsider f9 = f opp as Morphism of c opp ,b ;

thus A10: Hom ((c opp),b) <> {} by A8, Th4, A9; :: thesis: ex b

for b

take f9 ; :: thesis: for b

let g be Morphism of c opp ,b; :: thesis: f9 = g

opp g is Morphism of opp b, opp (c opp) by A10, Th13;

hence g = f by A7

.= f9 by Def6, A9 ;

:: thesis: verum