let C be Category; :: thesis: for f being Morphism of C holds
( f opp is invertible iff f is invertible )
let f be Morphism of C; :: thesis: ( f opp is invertible iff f is invertible )
thus ( f opp is invertible implies f is invertible ) :: thesis: ( f is invertible implies f opp is invertible )

proof

given g being Morphism of (C opp ) such that A1: ( dom g = cod (f opp ) & cod g = dom (f opp ) ) and
A2: ( (f opp ) * g = id (cod (f opp )) & g * (f opp ) = id (dom (f opp )) ) ; :: according to CAT_1:def 12 :: thesis: f is invertible
take g9 = opp g; :: according to CAT_1:def 12 :: thesis: ( dom g9 = cod f & cod g9 = dom f & f * g9 = id (cod f) & g9 * f = id (dom f) )
thus ( dom g9 = cod f & cod g9 = dom f ) by A1; :: thesis: ( f * g9 = id (cod f) & g9 * f = id (dom f) )
then ( (f * g9) opp = (g9 opp ) * (f opp ) & (g9 * f) opp = (f opp ) * (g9 opp ) ) by Th17;
hence ( f * g9 = id (cod f) & g9 * f = id (dom f) ) by A2; :: thesis: verum

end;

given g being Morphism of C such that A3: ( dom g = cod f & cod g = dom f ) and
A4: ( f * g = id (cod f) & g * f = id (dom f) ) ; :: according to CAT_1:def 12 :: thesis: f opp is invertible
take g opp ; :: according to CAT_1:def 12 :: thesis: ( dom (g opp ) = cod (f opp ) & cod (g opp ) = dom (f opp ) & (f opp ) * (g opp ) = id (cod (f opp )) & (g opp ) * (f opp ) = id (dom (f opp )) )
thus ( dom (g opp ) = cod (f opp ) & cod (g opp ) = dom (f opp ) ) by A3; :: thesis: ( (f opp ) * (g opp ) = id (cod (f opp )) & (g opp ) * (f opp ) = id (dom (f opp )) )
then ( (f * g) opp = (g opp ) * (f opp ) & (g * f) opp = (f opp ) * (g opp ) ) by Th18;
hence ( (f opp ) * (g opp ) = id (cod (f opp )) & (g opp ) * (f opp ) = id (dom (f opp )) ) by A4; :: thesis: verum