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