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 9 :: thesis: f is invertible
take g9 = opp g; :: according to CAT_1:def 9 :: 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 9 :: thesis: f opp is invertible
take g opp ; :: according to CAT_1:def 9 :: 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