let C be non empty category; :: thesis: 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; :: 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 )
assume a,b are_isomorphic ; :: thesis: 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; :: according to CAT_8:def 2 :: 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;
Hom (c,b) <> {} by A1;
hence A5: Hom (c,a) <> {} by A3, CAT_7:22; :: thesis: 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 ; :: thesis: for g being Morphism of c,a holds f1 * h = g
let h1 be Morphism of c,a; :: thesis: 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 ; :: thesis: verum