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 b₁ being Morphism of a opp ,b opp holds
( not (f opp) * b₁ = id (a opp) or not b₁ * (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 A1, Th4; :: according to CAT_1:def 16 :: thesis: ex b₁ being Morphism of b,a st
( f * b₁ = id b & b₁ * 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 Def6, A3
.= gg by Def7, A1 ;
thus f * g = (g opp) * (f opp) by A3, Lm3
.= id (b opp) by A2, A4
.= id b by Lm2 ; :: thesis: g * f = id a
thus g * f = (f opp) * (g opp) by A3, Lm3
.= 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 b₁ being Morphism of b,a holds
( not f * b₁ = id b or not b₁ * 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: f opp is invertible
thus ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) by A5, Th4; :: according to CAT_1:def 16 :: thesis: ex b₁ being Morphism of a opp ,b opp st
( (f opp) * b₁ = id (a opp) & b₁ * (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 A5, Lm3
.= id (a opp) by A6, Lm2 ; :: thesis: (g opp) * (f opp) = id (b opp)
thus (g opp) * (f opp) = f * g by A5, Lm3
.= id (b opp) by A6, Lm2 ; :: thesis: verum