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

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

end;

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