let C be Category; :: thesis: for a, b being Object of C
for f being Morphism of a,b holds
( f opp is invertible iff f is invertible )

let a, b be Object of C; :: thesis: for f being Morphism of a,b holds
( f opp is invertible iff f is invertible )

let f be Morphism of a,b; :: 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
assume A1: ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) ; :: according to CAT_1:def 16 :: thesis: ( for b1 being Morphism of a opp ,b opp holds
( not (f opp) * b1 = id (a opp) or not b1 * (f opp) = id (b opp) ) or f is invertible )

given gg being Morphism of a opp ,b opp such that A2: ( (f opp) * gg = id (a opp) & gg * (f opp) = id (b opp) ) ; :: thesis: f is invertible
thus A3: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by ; :: according to CAT_1:def 16 :: thesis: ex b1 being Morphism of b,a st
( f * b1 = id b & b1 * f = id a )

reconsider g = opp gg as Morphism of b,a ;
take g ; :: thesis: ( f * g = id b & g * f = id a )
A4: g opp = g by
.= gg by ;
thus f * g = (g opp) * (f opp) by
.= id (b opp) by A2, A4
.= id b by Lm2 ; :: thesis: g * f = id a
thus g * f = (f opp) * (g opp) by
.= id a by A2, A4, Lm2 ; :: thesis: verum
end;
assume A5: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_1:def 16 :: thesis: ( for b1 being Morphism of b,a holds
( not f * b1 = id b or not b1 * f = id a ) or f opp is invertible )

given g being Morphism of b,a such that A6: ( f * g = id b & g * f = id a ) ; :: thesis:
thus ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) by ; :: according to CAT_1:def 16 :: thesis: ex b1 being Morphism of a opp ,b opp st
( (f opp) * b1 = id (a opp) & b1 * (f opp) = id (b opp) )

take g opp ; :: thesis: ( (f opp) * (g opp) = id (a opp) & (g opp) * (f opp) = id (b opp) )
thus (f opp) * (g opp) = g * f by
.= id (a opp) by ; :: thesis: (g opp) * (f opp) = id (b opp)
thus (g opp) * (f opp) = f * g by
.= id (b opp) by ; :: thesis: verum