let C be Category; :: thesis: 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; :: thesis: ( a is initial & b is initial implies a,b are_isomorphic )
assume that
A1: a is initial and
A2: b is initial ; :: thesis: a,b are_isomorphic
set g = the Morphism of b,a;
set f = the Morphism of a,b;
A3: Hom (a,b) <> {} by A1;
take the Morphism of a,b ; :: according to CAT_1:def 20 :: thesis: the Morphism of a,b is invertible

now :: thesis: ( 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 A2; :: thesis: 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; :: thesis: ( 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, Th45; :: thesis: verum

end;

hence the Morphism of a,b is invertible by A3; :: thesis: verum