let C be Category; :: thesis: for f being Morphism of C holds
( f is invertible iff ( f is retraction & f is coretraction ) )
let f be Morphism of C; :: 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 ex g being Morphism of C st
( dom g = cod f & cod g = dom f & f * g = id (cod f) & g * f = id (dom f) ) ; :: according to CAT_1:def 12 :: thesis: ( f is retraction & f is coretraction )
hence ( f is retraction & f is coretraction ) by Def10, Def11; :: 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 Th26, Th33; :: thesis: verum