let C be Category; for a, b being Object of C st a is terminal & b is terminal holds
a,b are_isomorphic
let a, b be Object of C; ( a is terminal & b is terminal implies a,b are_isomorphic )
assume that
A1:
a is terminal
and
A2:
b is terminal
; a,b are_isomorphic
set g = the Morphism of b,a;
set f = the Morphism of a,b;
thus A3:
Hom (a,b) <> {}
by A2, Def15; CAT_1:def 14 ex f being Morphism of a,b st f is invertible
take
the Morphism of a,b
; the Morphism of a,b is invertible
now thus
Hom (
b,
a)
<> {}
by A1, Def15;
ex g being Morphism of b,a st
( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a )take g = the
Morphism of
b,
a;
( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a )thus
( the
Morphism of
a,
b * g = id b &
g * the
Morphism of
a,
b = id a )
by A1, A2, Th87;
verum end;
hence
the Morphism of a,b is invertible
by A3, Th70; verum