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;
A3:
Hom (a,b) <> {}
by A2;
take
the Morphism of a,b
; CAT_1:def 20 the Morphism of a,b is invertible
now ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( the Morphism of a,b * g = id b & g * the Morphism of a,b = id a ) )thus
Hom (
b,
a)
<> {}
by A1;
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, Th49;
verum end;
hence
the Morphism of a,b is invertible
by A3; verum