let C be Category; :: thesis: for a, b being Object of C
for f being Morphism of a,b holds
( f is invertible iff ( f is retraction & f is coretraction ) )
let a, b be Object of C; :: thesis: for f being Morphism of a,b holds
( f is invertible iff ( f is retraction & f is coretraction ) )
let f be Morphism of a,b; :: thesis: ( f is invertible iff ( f is retraction & f is coretraction ) )
thus ( f is invertible implies ( f is retraction & f is coretraction ) ) :: thesis: ( f is retraction & f is coretraction implies f is invertible )

proof

assume A1: ( 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 is retraction & f is coretraction ) )
assume ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ; :: thesis: ( f is retraction & f is coretraction )
hence ( f is retraction & f is coretraction ) by A1, Def8, Def9; :: thesis: verum

end;

assume f is retraction ; :: thesis: ( not f is coretraction or f is invertible )
hence ( not f is coretraction or f is invertible ) by Th22, Th29; :: thesis: verum