let C be Category; :: thesis: for a, b being Object of C holds
( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) )
let a, b be Object of C; :: thesis: ( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) )
thus ( a,b are_isomorphic implies ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) ) :: thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) implies a,b are_isomorphic )

proof

assume A1: Hom (a,b) <> {} ; :: according to CAT_1:def 17 :: thesis: ( for f being Morphism of a,b holds not f is invertible or ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) )
given f being Morphism of a,b such that A2: f is invertible ; :: thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) )
thus ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1, A2, Th70; :: thesis: ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a )
take f ; :: thesis: ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a )
thus ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) by A1, A2, Th70; :: thesis: verum

end;

assume that
A3: Hom (a,b) <> {} and
A4: Hom (b,a) <> {} ; :: thesis: ( for f being Morphism of a,b
for f9 being Morphism of b,a holds
( not f * f9 = id b or not f9 * f = id a ) or a,b are_isomorphic )
given f being Morphism of a,b such that A5: ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ; :: thesis: a,b are_isomorphic
thus Hom (a,b) <> {} by A3; :: according to CAT_1:def 17 :: thesis: ex f being Morphism of a,b st f is invertible
take f ; :: thesis: f is invertible
thus f is invertible by A3, A4, A5, Th70; :: thesis: verum