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

proof

given g being Morphism of C such that A2: ( dom g = cod f & cod g = dom f ) and
A3: ( f * g = id (cod f) & g * f = id (dom f) ) ; :: according to CAT_1:def 12 :: thesis: ( Hom b,a <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) )
A4: ( dom f = a & cod f = b ) by A1, Th23;
hence A5: Hom b,a <> {} by A2, Th18; :: thesis: ex g being Morphism of b,a st
( f * g = id b & g * f = id a )
reconsider g = g as Morphism of b,a by A2, A4, Th22;
take g ; :: thesis: ( f * g = id b & g * f = id a )
thus ( f * g = id b & g * f = id a ) by A1, A3, A4, A5, Def13; :: thesis: verum

end;

assume A6: Hom b,a <> {} ; :: thesis: ( for g being Morphism of b,a holds
( not f * g = id b or not g * f = id a ) or f is invertible )
given g being Morphism of b,a such that A7: ( f * g = id b & g * f = id a ) ; :: thesis: f is invertible
reconsider g = g as Morphism of C ;
take g ; :: according to CAT_1:def 12 :: thesis: ( dom g = cod f & cod g = dom f & f * g = id (cod f) & g * f = id (dom f) )
( dom f = a & cod f = b ) by A1, Th23;
hence ( dom g = cod f & cod g = dom f & f * g = id (cod f) & g * f = id (dom f) ) by A1, A6, A7, Def13, Th23; :: thesis: verum