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 A2: f is invertible ; :: thesis: ex f being Morphism of b,a st f is invertible
A3: ( Hom (b,a) <> {} & Hom (a,b) <> {} ) by A2, Dfi;
consider g being Morphism of b,a such that
A4: ( f * g = id b & g * f = id a ) by A2, Dfi;
take g ; :: thesis: g is invertible
thus g is invertible by A3, A4, Dfi; :: thesis: verum