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

proof

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