let C be non empty composable with_identities CategoryStr ; for a, b being Object of C st a is initial & b is initial holds
a,b are_isomorphic
let a, b be Object of C; ( a is initial & b is initial implies a,b are_isomorphic )
assume that
A1:
a is initial
and
A2:
b is initial
; a,b are_isomorphic
set g = the Morphism of b,a;
set f = the Morphism of a,b;
A3:
Hom (b,a) <> {}
by A2;
the Morphism of a,b is isomorphism
proof
A4:
Hom (
a,
b)
<> {}
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, Th31;
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