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