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 10 :: thesis: f opp is coretraction
take i opp ; :: according to CAT_3:def 11 :: 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:9
.= cod (f opp ) by OPPCAT_1:9 ; :: thesis: (i opp ) * (f opp ) = id (dom (f opp ))
thus (i opp ) * (f opp ) = (id (cod f)) opp by A1, A2, OPPCAT_1:17
.= id ((cod f) opp ) by OPPCAT_1:21
.= id (dom (f opp )) by OPPCAT_1:11 ; :: 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 11 :: thesis: f is retraction
take opp i ; :: according to CAT_3:def 10 :: thesis: ( cod (opp i) = dom f & f * (opp i) = id (cod f) )
thus A5: cod (opp i) = cod (f opp ) by A3, OPPCAT_1:10
.= dom f by OPPCAT_1:9 ; :: 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:17
.= id (dom (f opp )) by A4, OPPCAT_1:8
.= id ((cod f) opp ) by OPPCAT_1:11
.= (id (cod f)) opp by OPPCAT_1:21
.= id (cod f) by OPPCAT_1:def 4 ; :: thesis: verum