hereby ( 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
a,
b are_isomorphic
;
( 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;
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;
ex g being Morphism of b,a st
( g * f = id- a & f * g = id- b )take g =
g;
( g * f = id- a & f * g = id- b )thus
(
g * f = id- a &
f * g = id- b )
by A2;
verum
end;
assume A3:
( Hom (a,b) <> {} & Hom (b,a) <> {} )
; ( for f being Morphism of a,b
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 )
; a,b are_isomorphic
f is isomorphism
by A3, A4;
hence
a,b are_isomorphic
; verum