let C be Category; :: thesis: for b, a being Object of C st b is terminal & a,b are_isomorphic holds
a is terminal
let b, a be Object of C; :: thesis: ( b is terminal & a,b are_isomorphic implies a is terminal )
assume A1: b is terminal ; :: thesis: ( not a,b are_isomorphic or a is terminal )
given f being Morphism of a,b such that A2: f is invertible ; :: according to CAT_1:def 20 :: thesis: a is terminal
A3: Hom (b,a) <> {} by A2, Dfi;
let c be Object of C; :: according to CAT_1:def 18 :: thesis: ( 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, Def12;
Hom (c,b) <> {} by A1, Def12;
hence A5: Hom (c,a) <> {} by A3, Th23; :: thesis: ex f being Morphism of c,a st
for g being Morphism of c,a holds f = g
consider f9 being Morphism of b,a such that
f * f9 = id b and
A6: f9 * f = id a by A2, Dfi;
A7: Hom (a,b) <> {} by A2, Dfi;
take f9 * h ; :: thesis: for g being Morphism of c,a holds f9 * h = g
let h9 be Morphism of c,a; :: thesis: f9 * h = h9
thus f9 * h = f9 * (f * h9) by A4
.= (f9 * f) * h9 by A3, A5, A7, Th25
.= h9 by A6, A5, Th28 ; :: thesis: verum