let C be Category; :: thesis: for f being Morphism of C holds
( f is retraction iff f opp is coretraction )
let f be Morphism of C; :: 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

given i being Morphism of C such that A1: cod i = dom f and
A2: f * i = id (cod f) ; :: according to CAT_3:def 8 :: thesis: f opp is coretraction
take i opp ; :: according to CAT_3:def 9 :: thesis: ( dom (i opp) = cod (f opp) & (i opp) * (f opp) = id (dom (f opp)) )
thus dom (i opp) = dom f by A1, OPPCAT_1:8
.= cod (f opp) by OPPCAT_1:8 ; :: thesis: (i opp) * (f opp) = id (dom (f opp))
thus (i opp) * (f opp) = (id (cod f)) opp by A1, A2, OPPCAT_1:16
.= id ((cod f) opp) by OPPCAT_1:20
.= id (dom (f opp)) by OPPCAT_1:10 ; :: thesis: verum

end;

given i being Morphism of (C opp) such that A3: dom i = cod (f opp) and
A4: i * (f opp) = id (dom (f opp)) ; :: according to CAT_3:def 9 :: thesis: f is retraction
take opp i ; :: according to CAT_3:def 8 :: thesis: ( cod (opp i) = dom f & f * (opp i) = id (cod f) )
thus A5: cod (opp i) = cod (f opp) by A3, OPPCAT_1:9
.= dom f by OPPCAT_1:8 ; :: thesis: f * (opp i) = id (cod f)
thus f * (opp i) = (f * (opp i)) opp by OPPCAT_1:def 4
.= ((opp i) opp) * (f opp) by A5, OPPCAT_1:16
.= id (dom (f opp)) by A4, OPPCAT_1:7
.= id ((cod f) opp) by OPPCAT_1:10
.= (id (cod f)) opp by OPPCAT_1:20
.= id (cod f) by OPPCAT_1:def 4 ; :: thesis: verum