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

( c is initial iff c opp is terminal )

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

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

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

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

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

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

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

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

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

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

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

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

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

g opp = f by A7;

hence g = f by Def6, A10

.= f9 by A9, Def7 ;

:: thesis: verum

( c is initial iff c opp is terminal )

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

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

proof

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

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

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

consider f being Morphism of c, opp b such that

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

A3: (opp b) opp = b ;

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

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

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

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

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

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

opp (c opp) = c ;

then opp g is Morphism of c, opp b by A5, Th13;

hence g = f by A2

.= f9 by A4, Def6 ;

:: thesis: verum

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

for b

consider f being Morphism of c, opp b such that

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

A3: (opp b) opp = b ;

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

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

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

for b

take f9 ; :: thesis: for b

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

opp (c opp) = c ;

then opp g is Morphism of c, opp b by A5, Th13;

hence g = f by A2

.= f9 by A4, Def6 ;

:: thesis: verum

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

for b

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

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

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

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

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

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

for b

take f9 ; :: thesis: for b

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

g opp = f by A7;

hence g = f by Def6, A10

.= f9 by A9, Def7 ;

:: thesis: verum