let a, b be Object of C; :: thesis: ( ex f being Morphism of a,b st f is invertible implies ex f being Morphism of b,a st f is invertible )
given f being Morphism of a,b such that A1: f is invertible ; :: thesis: ex f being Morphism of b,a st f is invertible
A2: ( Hom (b,a) <> {} & Hom (a,b) <> {} ) by A1;
consider g being Morphism of b,a such that
A3: ( f * g = id b & g * f = id a ) by A1;
take g ; :: thesis: g is invertible
thus g is invertible by A2, A3; :: thesis: verum