let C be Category; :: thesis: 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; :: thesis: ( a is initial & a,b are_isomorphic implies b is initial )
assume that
A1: a is initial and
A2: a,b are_isomorphic ; :: thesis: b is initial
A3: Hom (b,a) <> {} by A2, Th81;
let c be Object of C; :: according to CAT_1:def 13 :: thesis: ( 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, Def16;
Hom (a,c) <> {} by A1, Def16;
hence A5: Hom (b,c) <> {} by A3, Th51; :: thesis: ex f being Morphism of b,c st
for g being Morphism of b,c holds f = g
consider f being Morphism of a,b, f9 being Morphism of b,a such that
A6: f * f9 = id b and
f9 * f = id a by A2, Th81;
A7: Hom (a,b) <> {} by A2, Def17;
take h * f9 ; :: thesis: for g being Morphism of b,c holds h * f9 = g
let h9 be Morphism of b,c; :: thesis: h * f9 = h9
thus h9 = h9 * (f * f9) by A6, A5, Th58
.= (h9 * f) * f9 by A3, A5, A7, Th54
.= h * f9 by A4 ; :: thesis: verum