hereby :: thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex g being Morphism of b,a st

( g * f = id- a & f * g = id- b ) implies a,b are_isomorphic )

assume A3:
( Hom (a,b) <> {} & Hom (b,a) <> {} )
; :: thesis: ( for f being Morphism of a,b( g * f = id- a & f * g = id- b ) implies a,b are_isomorphic )

assume
a,b are_isomorphic
; :: thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex g being Morphism of b,a st

( g * f = id- a & f * g = id- b ) )

then consider f being Morphism of a,b such that

A1: f is isomorphism ;

thus ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1; :: thesis: ex f being Morphism of a,b ex g being Morphism of b,a st

( g * f = id- a & f * g = id- b )

consider g being Morphism of b,a such that

A2: ( g * f = id- a & f * g = id- b ) by A1;

take f = f; :: thesis: ex g being Morphism of b,a st

( g * f = id- a & f * g = id- b )

take g = g; :: thesis: ( g * f = id- a & f * g = id- b )

thus ( g * f = id- a & f * g = id- b ) by A2; :: thesis: verum

end;( g * f = id- a & f * g = id- b ) )

then consider f being Morphism of a,b such that

A1: f is isomorphism ;

thus ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1; :: thesis: ex f being Morphism of a,b ex g being Morphism of b,a st

( g * f = id- a & f * g = id- b )

consider g being Morphism of b,a such that

A2: ( g * f = id- a & f * g = id- b ) by A1;

take f = f; :: thesis: ex g being Morphism of b,a st

( g * f = id- a & f * g = id- b )

take g = g; :: thesis: ( g * f = id- a & f * g = id- b )

thus ( g * f = id- a & f * g = id- b ) by A2; :: thesis: verum

for g being Morphism of b,a holds

( not g * f = id- a or not f * g = id- b ) or a,b are_isomorphic )

given f being Morphism of a,b, g being Morphism of b,a such that A4: ( g * f = id- a & f * g = id- b ) ; :: thesis: a,b are_isomorphic

f is isomorphism by A3, A4;

hence a,b are_isomorphic ; :: thesis: verum