let C be non empty category; for a, b being Object of C st b is terminal & a,b are_isomorphic holds
a is terminal
let a, b be Object of C; ( b is terminal & a,b are_isomorphic implies a is terminal )
assume A1:
b is terminal
; ( not a,b are_isomorphic or a is terminal )
assume
a,b are_isomorphic
; a is terminal
then consider f being Morphism of a,b such that
A2:
f is isomorphism
by CAT_7:def 10;
A3:
Hom (b,a) <> {}
by A2, CAT_7:def 9;
let c be Object of C; CAT_8:def 2 ( Hom (c,a) <> {} & ex f being Morphism of c,a st
for g being Morphism of c,a holds f = g )
consider h being Morphism of c,b such that
A4:
for g being Morphism of c,b holds h = g
by A1;
Hom (c,b) <> {}
by A1;
hence A5:
Hom (c,a) <> {}
by A3, CAT_7:22; ex f being Morphism of c,a st
for g being Morphism of c,a holds f = g
consider f1 being Morphism of b,a such that
A6:
f1 * f = id- a
and
f * f1 = id- b
by A2, CAT_7:def 9;
A7:
Hom (a,b) <> {}
by A2, CAT_7:def 9;
take
f1 * h
; for g being Morphism of c,a holds f1 * h = g
let h1 be Morphism of c,a; f1 * h = h1
thus f1 * h =
f1 * (f * h1)
by A4
.=
(f1 * f) * h1
by A3, A5, A7, CAT_7:23
.=
h1
by A6, A5, CAT_7:18
; verum