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

proof

assume A1: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_3:def 9 :: thesis: ( for g being Morphism of b,a holds not g * f = id a or f opp is retraction )
given i being Morphism of b,a such that A2: i * f = id a ; :: thesis: f opp is retraction
thus ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) by A1, OPPCAT_1:5; :: according to CAT_3:def 8 :: thesis: ex g being Morphism of a opp ,b opp st (f opp) * g = id (a opp)
take i opp ; :: thesis: (f opp) * (i opp) = id (a opp)
thus (f opp) * (i opp) = id a by A1, A2, OPPCAT_1:70
.= id (a opp) by OPPCAT_1:71 ; :: thesis: verum

end;

assume A3: ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) ; :: according to CAT_3:def 8 :: thesis: ( for g being Morphism of a opp ,b opp holds not (f opp) * g = id (a opp) or f is coretraction )
given i being Morphism of a opp ,b opp such that A4: (f opp) * i = id (a opp) ; :: thesis: f is coretraction
thus A5: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A3, OPPCAT_1:5; :: according to CAT_3:def 9 :: thesis: ex g being Morphism of b,a st g * f = id a
take opp i ; :: thesis: (opp i) * f = id a
(opp i) opp = opp i by A5, OPPCAT_1:def 6
.= i by A3, OPPCAT_1:def 7 ;
hence (opp i) * f = (f opp) * i by A5, OPPCAT_1:70
.= id (a opp) by A4
.= id a by OPPCAT_1:71 ;
:: thesis: verum