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

assume A2: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_1:def 16 :: thesis: ( for g being Morphism of b,a holds
( not f * g = id b or not g * f = id a ) or ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) )
given g being Morphism of b,a such that A3: ( 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 ) )
thus Hom (b,a) <> {} by A2; :: thesis: ex g being Morphism of b,a st
( f * g = id b & g * f = id a )
take g ; :: thesis: ( f * g = id b & g * f = id a )
thus ( f * g = id b & g * f = id a ) by A3; :: 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
thus ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1, A6; :: according to CAT_1:def 16 :: thesis: ex g being Morphism of b,a st
( f * g = id b & g * f = id a )
take g ; :: thesis: ( f * g = id b & g * f = id a )
thus ( f * g = id b & g * f = id a ) by A7; :: thesis: verum