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
consider g being Morphism of b,a;
consider f being Morphism of a,b;
thus A3: Hom a,b <> {} by A1, Def16; :: according to CAT_1:def 17 :: thesis: ex f being Morphism of a,b st f is invertible
take f ; :: thesis: f is invertible

now

thus Hom b,a <> {} by A2, Def16; :: thesis: ex g being Morphism of b,a st
( f * g = id b & g * f = id a )
take g = g; :: thesis: ( f * g = id b & g * f = id a )
thus ( f * g = id b & g * f = id a ) by A1, A2, Th83; :: thesis: verum

end;

hence f is invertible by A3, Th70; :: thesis: verum