let C be Category; for a, b being Object of C st a is initial & a,b are_isomorphic holds
b is initial
let a, b be Object of C; ( a is initial & a,b are_isomorphic implies b is initial )
assume A1:
a is initial
; ( not a,b are_isomorphic or b is initial )
given f being Morphism of a,b such that A2:
f is invertible
; CAT_1:def 20 b is initial
A3:
Hom (b,a) <> {}
by A2;
let c be Object of C; CAT_1:def 19 ( Hom (b,c) <> {} & ex f being Morphism of b,c st
for g being Morphism of b,c holds f = g )
consider h being Morphism of a,c such that
A4:
for g being Morphism of a,c holds h = g
by A1;
Hom (a,c) <> {}
by A1;
hence A5:
Hom (b,c) <> {}
by A3, Th19; ex f being Morphism of b,c st
for g being Morphism of b,c holds f = g
consider f9 being Morphism of b,a such that
A6:
f * f9 = id b
and
f9 * f = id a
by A2;
A7:
Hom (a,b) <> {}
by A2;
take
h * f9
; for g being Morphism of b,c holds h * f9 = g
let h9 be Morphism of b,c; h * f9 = h9
thus h9 =
h9 * (f * f9)
by A6, A5, Th24
.=
(h9 * f) * f9
by A3, A5, A7, Th21
.=
h * f9
by A4
; verum