let C be non empty composable with_identities CategoryStr ; 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;
the Morphism of a,b is isomorphism
proof
A4:
Hom (
b,
a)
<> {}
by A1;
( the
Morphism of
b,
a * the
Morphism of
a,
b = id- a & the
Morphism of
a,
b * the
Morphism of
b,
a = id- b )
by A1, A2, Th20;
hence
the
Morphism of
a,
b is
isomorphism
by A3, A4, CAT_7:def 9;
verum
end;
hence
a,b are_isomorphic
by CAT_7:def 10; verum